[isabelle-dev] Bash subcommand completion for isabelle
makarius at sketis.net
Mon Sep 26 10:58:33 CEST 2011
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.
More information about the isabelle-dev