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
begin
ML{*
val newline = writeln ""
*}
end

Now in isabelle_process I do:

use_thy "TestML"

The basic question is how do I access the value newline in the isabelle_process?

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 the theory?

Viorel




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