Re: [isabelle] find sessions



Am 12.11.2013 18:01, schrieb Makarius:
>> 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.

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


val options = isabelle.Options.init()
val path = isabelle.Path.explode("/home/necoro/cava")
val sessions = isabelle.Build.find_sessions(options, List((false, path)))

sessions.graph.keys.foreach{ s => print(s + " ") }
println


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

I don't know yet, if I want this to be called from a shell script.

- René

-- 
René Neumann

Institut für Informatik (I7)
Technische Universität München
Boltzmannstr. 3
85748 Garching b. München

Tel: +49-89-289-17232
Office: MI 03.11.055

Attachment: smime.p7s
Description: S/MIME Kryptografische Unterschrift



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