[isabelle-dev] Bash subcommand completion for isabelle

[Makarius]

On Mon, 26 Sep 2011, Florian Haftmann wrote:

> An aside: have there ever been thoughts about adding subcommand 
> completion for isabelle in bash?  At first sight this looks as a nice 
> thing to have, but maybe there have been deeper consideration *not* to 
> attempt this.

There are no deeper reasons why it was not done so far.  When the old 
"isatool" now "isabelle" wrapper was introduced in 1996, bash completion 
was not as configurable as it is now.  Even the list of the available 
subcommands was crude and slow -- I have rewritting it in perl only a few 
months ago to make it more smooth.

Generally, my tendency is to reduce the importance of command line tools. 
Pretty soon there should be the Isabelle/Scala based "isabelle build" 
tool, which would also work directly in the Prover IDE. This does not mean 
that the terminal will disappear, but many users on Mac OS and Windows do 
not know what it is in the first place.


 	Makarius