Re: [isabelle] Presenting theories without running a session
On Mon, 14 Feb 2011, Christian Sternagel wrote:
I think what Robert finds strange (and me too, by the way), is that even
if using an (due to the message) existing flag like "-?", Isabelle
produces an error message before giving the usage information. Typing
isabelle usedir -?
isabelle usedir "-?"
isabelle usedir '-?'
in bash, using Isabelle2011 (down to at least Isabelle2007), I always
get the error message "illegal option -- ?".
But you did get the usage, right? The error is a known feature, because
"?" is not an option.
Over many years Isabelle shell scripts have converged towards a certain
standard form that minimizes various real problems, like spaces or unicode
in directory names. It all has become surprisingly complex, and indeed
the semantics of bash is very complicated. Any adhoc changes in the
scripts to do not really make a fundamental difference are likely to
increase the entropy.
Generally, there is a tendency to reduce traditional shell exposure of
Isabelle more and more, as the Isabelle/Scala layer takes over the main
responsibility of system integration. (Many users on Mac OS X and Windows
do not even know what a command-line based shell is and even failed to
do the "tar" invokations on the download site.)
This archive was generated by a fusion of
Pipermail (Mailman edition) and