equal
deleted
inserted
replaced
28 (OuterKeyword.tag "TutorialML" OuterKeyword.prf_decl) |
28 (OuterKeyword.tag "TutorialML" OuterKeyword.prf_decl) |
29 (OuterParse.ML_source >> (fn (txt, pos) => |
29 (OuterParse.ML_source >> (fn (txt, pos) => |
30 Toplevel.proof (Proof.map_context (Context.proof_map |
30 Toplevel.proof (Proof.map_context (Context.proof_map |
31 (ML_Context.exec (fn () => ML_Context.eval true pos txt))) #> inherit_env_prf))) |
31 (ML_Context.exec (fn () => ML_Context.eval true pos txt))) #> inherit_env_prf))) |
32 |
32 |
|
33 val _ = |
|
34 OuterSyntax.command "ML_val" "diagnostic ML text" |
|
35 (OuterKeyword.tag "TutorialML" OuterKeyword.diag) |
|
36 (OuterParse.ML_source >> IsarCmd.ml_diag true); |
|
37 |
33 *} |
38 *} |
34 (* |
39 (* |
35 ML {* |
40 ML {* |
36 fun warning str = str |
41 fun warning str = str |
37 fun tracing str = str |
42 fun tracing str = str |