[isabelle-dev] NEWS: more options for "isabelle jedit"
florian.haftmann at informatik.tu-muenchen.de
Sat Nov 4 10:25:24 CET 2017
> *** Prover IDE -- Isabelle/Scala/jEdit ***
> * The command-line tool "isabelle jedit" provides more flexible options
> for session selection:
> - options -P opens the parent session image of -l
> - options -A and -B modify the meaning of -l to produce a base
> image on the spot, based on the specified ancestor (or parent)
> - option -F focuses on the specified logic session
> - option -R has changed: it only opens the session ROOT entry
> - option -S sets up the development environment to edit the
> specified session: it abbreviates -B -F -R -l
> isabelle jedit -d '$AFP' -S Formal_SSA -A HOL
> isabelle jedit -d '$AFP' -S Formal_SSA -A HOL-Analysis
this is really great and makes my life significantly easier!
There remains one gap which I am wondering how to fill it.
Lets start with
isabelle jedit -d '$AFP' -S …
This provides a suitable base image and opens the ROOT file.
What is the canonical way to proceed from there to check the whole
session? Of course the ROOT file lists the respective theories and you
can open them manually in jedit, but this is tiresome if the ROOT file
spans many theories.
Would clicakble theorie files in ROOT files be an option?
-------------- next part --------------
A non-text attachment was scrubbed...
Size: 819 bytes
Desc: OpenPGP digital signature
More information about the isabelle-dev