Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] -l flag

view this post on Zulip Email Gateway (Aug 18 2022 at 14:00):

From: Christian Sternagel <christian.sternagel@uibk.ac.at>
It seems as if

$ isabelle emacs -l image file

does not work as

$ Isabelle -l image file

did. I do not get any error-message, but end up using the Default image.
What is the new way of specifying the image to use on startup?

cheers

christian

view this post on Zulip Email Gateway (Aug 18 2022 at 14:01):

From: Makarius <makarius@sketis.net>
Strange this should work. In both cases, the Isabelle script is merely a
wrapper to ProofGeneral/isar/interface.

Of course, there might be a problem in invoking the correct one in the
first place. You can easily see what bash does by adding "set -x" near
the beginning of Isabelle2009/lib/Tools/emacs or
ProofGeneral/isar/interface -- the latter will set PROOFGENERAL_LOGIC in
the very end, before invoking Emacs with Proof General.

Makarius

Last updated: May 06 2024 at 12:29 UTC