Re: [isabelle] find sessions

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

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

I just came up with this little Scala-snippet, that seems to do what I
need (first time ever I touched Scala):

So far the question what you actually need was left open.

Isabelle/jEdit already provides a dialog to select the logic image, and it is rebuilt automatically on startup. The reboot is a bit awkward, but it should usually do the job.

Unfortunately, this is rather slow. Both the startup (ie running isabelle_scala_script), and also the Options.init() and find_sessions().

By making a cold start from outside the Isabelle system, e.g. from the shell, several startup-penalties are adding up: Scala script compilation, JVM runtime warmup etc.

There are ways to reduce this a bit, although I am myself not an expert of all the options to scalac and java runtime.

The general move in recent years is away from Isabelle command-line tools, and towards the assumption that you have the Prover IDE already running and do things from there.


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