[isabelle] An 'isabelle emacs' wrapper



Hi,

I just wanted to share a small script I created to have a more
convenient 'isabelle emacs' behavior: Especially when dealing with
different logic images, it is quite cumbersome to manually change the
image in PG each time you open a file needing a special image.

This script should change this:

1.) It can be passed a logic-pattern: This pattern is matched against
all logics as returned by `isabelle findlogics` and then the first match
is taken:
	So if you have 'HOL HOL-Cava-Libs HOL-Graphs HOL-Library Pure' as
images, "C" would match 'HOL-Cava-Libs' as would "L" (first match wins).

2.) This behavior is nice, but when working with the very same project
over and over, it is again cumbersome. Therefore the script also is able
to evaluate the file ".isabelle-logic" in the current directory. This
file should contain exactly one line with the image name (it is taken as
a pattern, but spelling out the complete name is probably better to
avoid surprises).
If the file contains "..", ../.isabelle-logic is looked up (this works
recursively).

So perhaps someone finds this useful. Feel free to edit/enhance it as
you like :).

- René

P.S.: By specifiying the logic during startup the chooser in the menu in
PG is not altered(!), hence always states "HOL". The correct image is
nevertheless loaded when starting isabelle from PG.

P.P.S.: The script is a ported version of a personal zsh-script of mine.
It may therefore contain constructs which look strange to a bash-user :)

Attachment: IE.sh
Description: Bourne shell script



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.