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