equal
deleted
inserted
replaced
8 (* to have a special tag for text enclosed in ML *) |
8 (* to have a special tag for text enclosed in ML *) |
9 ML {* |
9 ML {* |
10 |
10 |
11 val _ = |
11 val _ = |
12 OuterSyntax.command "ML" "eval ML text within theory" |
12 OuterSyntax.command "ML" "eval ML text within theory" |
13 (OuterKeyword.tag "CookBookML" OuterKeyword.thy_decl) |
13 (OuterKeyword.tag "TutorialML" OuterKeyword.thy_decl) |
14 (OuterParse.ML_source >> (fn (txt, pos) => |
14 (OuterParse.ML_source >> (fn (txt, pos) => |
15 Toplevel.generic_theory (ML_Context.exec (fn () => ML_Context.eval true pos txt)))); |
15 Toplevel.generic_theory (ML_Context.exec (fn () => ML_Context.eval true pos txt)))); |
16 *} |
16 *} |
17 |
17 |
18 |
18 |