Re: [isabelle] Running ML in a theory context from the command line



> Here is a complete example (with the included Scratch.thy):
> 
>   isabelle process -l Pure -T "~/Scratch" -e "fun eval_in_theory thy s =
> ML_Context.eval_source_in (SOME (Proof_Context.init_global thy))
> ML_Compiler.flags (Input.string s)" -e 'eval_in_theory
> (Thy_Info.get_theory "Draft.Scratch") "test (serial_string ())"'

Thanks, that should work.

> Maybe I should provide a function line eval_in_theory already in Pure.
> Are there further important applications?

I suppose all of the "tptp" tools, they use the same trick with a
temporary file. But Jasmin could say for sure.




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