Re: [isabelle] Presenting theories without running a session



On Wed, 16 Feb 2011 00:52:09 Makarius wrote:
> There is a misunderstanding here.  There is no option for help
> or usage, but you get the latter whenever the command line is
> syntactically malformed.  Passing "-?" provokes such a syntax
> error, so you get the usage of the command line as advertized.
>  This was part of my minimalistic design when I did this many
> years ago.
> 
> You can understand it as an instance of the original Unix
> attitude to avoid extra features if the same can be achieved
> as a consequence of existing functionality.  Or as an instance
> of the principle in logic that redundant axioms are avoided in
> favour of lemmas.

Is guess this partly depends on what you mean by "feature", and 
more specifically, whether you consider error messages to be 
ordinary features.  It seems strange to me that you're inviting 
users to obtain usage information by provoking an error, rather 
than by invoking a help or usage option.  You said yourself that 
"There is no option for help or usage".  I think this is what 
seemed strange to Robert, too.

Of course, it's not a big problem, because the usage information 
is available, but it could easily confuse users who are not used 
to having computer programs invite them to deliberately provoke 
errors.

Tim
<><

Attachment: signature.asc
Description: This is a digitally signed message part.



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