theory Base+ −
imports Main+ −
uses+ −
"chunks.ML"+ −
"antiquote_setup.ML"+ −
begin+ −
+ −
(* to have a special tag for text enclosed in ML *)+ −
ML {*+ −
+ −
val _ =+ −
OuterSyntax.command "ML" "eval ML text within theory"+ −
(OuterKeyword.tag "CookBookML" OuterKeyword.thy_decl)+ −
(OuterParse.ML_source >> (fn (txt, pos) =>+ −
Toplevel.generic_theory (ML_Context.exec (fn () => ML_Context.eval true pos txt))));+ −
*}+ −
+ −
+ −
end+ −