[isabelle-dev] NEWS: more options for "isabelle jedit"

Florian Haftmann florian.haftmann at informatik.tu-muenchen.de
Sat Nov 4 10:25:24 CET 2017


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

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 819 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20171104/943f82b7/attachment.sig>


More information about the isabelle-dev mailing list