Re: [isabelle] Presenting theories without running a session



On Mon, Feb 14, 2011 at 12:50 AM, Matthew Fernandez
<matthew.fernandez at nicta.com.au> wrote:
> 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.

Thanks, but actually I realized that. (I had been getting around it by
using double-quotes: "-?".)  I suppose that my point was, implicitly,
that it might be better to use a character which is never used as a
wildcard.  For instance, '-h' is common for many commands in the Linux
userspace.  I will acknowledge that if you are coming from the Windows
command shell, '-?' makes good sense.

Alternatively, Isabelle could use a scheme like certain version
control systems use: type "isabelle help" for general guidance and
"isabelle help TOOL" for guidance on the tool mentioned.  (Subversion
is an example of such a system.)

-- 
Robert





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