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
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Reply via email to