equal
deleted
inserted
replaced
12 OuterSyntax.command "ML" "eval ML text within theory" |
12 OuterSyntax.command "ML" "eval ML text within theory" |
13 (OuterKeyword.tag "TutorialML" 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 ML {* |
18 ML {* |
19 fun warning str = str |
19 fun warning str = str |
20 fun tracing str = str |
20 fun tracing str = str |
21 *} |
21 *} |
22 |
22 *) |
23 end |
23 end |