Re: [isabelle] Presenting theories without running a session



On 14/02/11 01:16, Makarius wrote:
On Thu, 10 Feb 2011, Robert Lamar wrote:

As an aside, here is something I noticed about the behavior of the
isabelle command line tool.  I can work around it, I am just sharing it
for your information as a possible bug: typing 'isabelle' at a command
prompt gives usage information, and includes the message 'pass "-?" for
tool specific help.' But if I type, say, 'isabelle usedir -?', it gives
the following message along with the expected usage info for usedir:

/scratch/usr/Isabelle2011/lib/Tools/usedir: illegal option -- ?


That is in bash.  In my favored shell, zsh, the shell gives an error
because it thinks the ? is a wildcard.

I've seen this effect for the last time with tcsh, many many years ago.

The usage message of the Isabelle scripts is correct in asking for "-?"
but it depends on the context how you need to produce that externally.
Here the context is prose English, so I have some quotes around it.  Bash
will accept it without quotes.  Other shells will have there own idea.

-\? does the trick in zsh, Robert.

Matthew.

The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.