Re: [isabelle] Presenting theories without running a session



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.


	Makarius





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