Re: [isabelle] accessing ML definitions in isabelle_process
On 4/28/2015 9:35 PM, Makarius wrote:
On Tue, 28 Apr 2015, Viorel Preoteasa wrote:
Using Isabelle/ML snippets inside a proper theory context seems
oriented towards a user interface. But I need to do this in batch
mode. If I use this approach I have to create always a theory file,
and then load it using use_thy. I would need to do this for every
small call that I need.
I was talking about batch mode already. You could e.g. put all your
tool setup in a static .thy (or .thy that loads a .ML via ML_file).
It could refer to some environment variables to get dynamic input from
somewhere else, e.g. another tmp file.
If I do this, and for example I define a value in a theory file:
theory TestML imports Main
val newline = writeln ""
Now in isabelle_process I do:
The basic question is how do I access the value newline in the
If I try just newline it is not recognized. Is this value available
under some scope?
Is it so that I am not supposed to access it from other place, except
This archive was generated by a fusion of
Pipermail (Mailman edition) and