[isabelle-dev] Bash subcommand completion for isabelle

Gerwin Klein gerwin.klein at nicta.com.au
Mon Sep 26 10:54:37 CEST 2011


On 26/09/2011, at 6:43 PM, 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.

I've been using the attached for a few years. Just load as part of your ~/.bashrc or similar.

It does 'isabelle make' target completion as well (code based on make completion from bash back then).

It probably needs a thorough code review before it can be put anywhere official. I've mostly used it just for myself, even though I think I sent it to isabelle-users at some point.

Cheers,
Gerwin


-------------- next part --------------
A non-text attachment was scrubbed...
Name: isabelle-completions
Type: application/octet-stream
Size: 1204 bytes
Desc: not available
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20110926/1efca193/attachment-0002.obj>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: PGP.sig
Type: application/pgp-signature
Size: 313 bytes
Desc: This is a digitally signed message part
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20110926/1efca193/attachment-0002.sig>


More information about the isabelle-dev mailing list