1 theory Base

     2 imports Main

     3 uses

     4   "chunks.ML"

     5   "antiquote_setup.ML"

     6 begin

     7 

     8 (* to have a special tag for text enclosed in ML *)

     9 ML {*

    10 

    11 val _ =

    12   OuterSyntax.command "ML" "eval ML text within theory"

    13     (OuterKeyword.tag "TutorialML" OuterKeyword.thy_decl)

    14     (OuterParse.ML_source >> (fn (txt, pos) =>

    15       Toplevel.generic_theory (ML_Context.exec (fn () => ML_Context.eval true pos txt))));

    16 *}

    17 (*

    18 ML {*

    19   fun warning str = str

    20   fun tracing str = str

    21 *}

    22 *)

    23 end