Email Gateway (Aug 18 2022 at 18:12): Email Gateway (Aug 18 2022 at 18:12):From: René Neumann <lists@necoro.eu>
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 :).
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 :)
IE.sh
Email Gateway (Aug 18 2022 at 18:12):From: René Neumann <lists@necoro.eu>
Short correction ... the debugging slipped in.
Email Gateway (Aug 18 2022 at 18:12):From: "Tim (McKenzie) Makarios" <tjm1983@gmail.com>
-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA1
I haven't looked at the script, but wouldn't "L" match 'HOL' first?
Tim
<><
-----BEGIN PGP SIGNATURE-----
Version: GnuPG v1.4.10 (GNU/Linux)
Comment: Using GnuPG with Mozilla - http://enigmail.mozdev.org/
iEYEARECAAYFAk5ITAYACgkQ/cBxZIxl6rmh9gCg2sQcTUsPp85YhSoiI3JzfjtL
3CsAoIwjBDkAO0elUERtyQuIuoocAb85
=fRE/
-----END PGP SIGNATURE-----
Email Gateway (Aug 18 2022 at 18:13):From: René Neumann <lists@necoro.eu>
Uh - of course. My fault, sorry.
Last updated: Apr 25 2024 at 04:18 UTC