Dear Makarius, > *** 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 > > Examples: > 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?
Cheers,
Florian
--
PGP available:
http://isabelle.in.tum.de/~haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
signature.asc
Description: OpenPGP digital signature
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
