[isabelle-dev] Options to pass to "isabelle jedit" after session directory reform

Makarius makarius at sketis.net
Thu Sep 26 15:31:28 CEST 2019


On 26/09/2019 15:20, Jasmin Blanchette wrote:
> 
> 	isabelle jedit -d ~/afp/thys Foo.thy
> 
> and that worked. (I also have 'init_component "$USER_HOME/afp"' in "~/.isabelle/etc/settings".)

With the init_component as above you can use -d '$AFP'

> But now (Isabelle/ffbe7784cc85 and AFP/66bfe59e1850) this has stopped
working. I get a red squiggly line under the import of
"Concurrent_Revisions.Operational_Semantics" in "Foo".

The theory name is actually "Concurrent_Revisions.OperationalSemantics"


> I studied the "isabelle jedit" options, as documented in "jedit.pdf", but couldn't figure out how to proceed. I'd be grateful for any hint.

Here is a changeset with the relevant NEWS entry:
https://isabelle.in.tum.de/repos/isabelle/rev/8c7706b053c7

The update to the documentation was rather minimal, because the text is
rather implicit about the important detail of session directory management.

After the reform it generally becomes simpler and faster, so there is
even less to say about it. Main point: session ROOT entries need to be
explicit about extra directories.


	Makarius


More information about the isabelle-dev mailing list