Re: [isabelle] find sessions



On Tue, 12 Nov 2013, René Neumann wrote:

There is 'isabelle findlogics', which gives me a list of all heaps.

findlogics is one of these obsolete Proof General tools. Its result is not well-defined, it merely lists files that happen to lie around in certain directories.


Is there some equivalent for sessions? Or would it be possible to add a switch to 'isabelle build'? So that e.g.

isabelle build -d . -L

just prints the list of sessions it can find?

Reason: Have a script select one from the list and pass it on as
'isabelle jedit -l $SESSION'

If it is not possible per se, but there is already some workaround needing some scripting, I'd be fine with this too.

You can either try to find suitable letter soups for "isabelle build" to approximate in the shell what you have in mind, or use Isabelle/Scala as the system programming language that it was meant to be. The "system" manual has a brief entry on the "Scala script wrapper".

Then you are in statically typed Isabelle/Scala, with access to the isabelle.Build module etc. So you can do "higher-order object-oriented scripting" there with the official Isabelle/Scala interfaces.


	Makarius


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.