theory Base
imports Main
uses
"output_tutorial.ML"
"chunks.ML"
"antiquote_setup.ML"
begin
(* to have a special tag for text enclosed in ML *)
ML {*
fun inherit_env (context as Context.Proof lthy) =
Context.Proof (LocalTheory.map_contexts (ML_Context.inherit_env context) lthy)
| inherit_env context = context;
fun inherit_env_prf prf = Proof.map_contexts
(Context.proof_map (ML_Context.inherit_env (Context.Proof (Proof.context_of prf)))) prf
val _ =
OuterSyntax.command "ML" "eval ML text within theory"
(OuterKeyword.tag "TutorialML" OuterKeyword.thy_decl)
(OuterParse.ML_source >> (fn (txt, pos) =>
Toplevel.generic_theory
(ML_Context.exec (fn () => ML_Context.eval true pos txt) #> inherit_env)));
val _ =
OuterSyntax.command "ML_prf" "ML text within proof"
(OuterKeyword.tag "TutorialML" OuterKeyword.prf_decl)
(OuterParse.ML_source >> (fn (txt, pos) =>
Toplevel.proof (Proof.map_context (Context.proof_map
(ML_Context.exec (fn () => ML_Context.eval true pos txt))) #> inherit_env_prf)))
val _ =
OuterSyntax.command "ML_val" "diagnostic ML text"
(OuterKeyword.tag "TutorialML" OuterKeyword.diag)
(OuterParse.ML_source >> IsarCmd.ml_diag true);
*}
end