| changeset 239 | b63c72776f03 |
| parent 224 | 647cab4a72c2 |
| child 255 | ef1da1abee46 |
| 238:29787dcf7b2e | 239:b63c72776f03 |
|---|---|
34 OuterSyntax.command "ML_val" "diagnostic ML text" |
34 OuterSyntax.command "ML_val" "diagnostic ML text" |
35 (OuterKeyword.tag "TutorialML" OuterKeyword.diag) |
35 (OuterKeyword.tag "TutorialML" OuterKeyword.diag) |
36 (OuterParse.ML_source >> IsarCmd.ml_diag true); |
36 (OuterParse.ML_source >> IsarCmd.ml_diag true); |
37 |
37 |
38 *} |
38 *} |
39 (* |
39 |
40 ML {* |
|
41 fun warning str = str |
|
42 fun tracing str = str |
|
43 *} |
|
44 *) |
|
45 end |
40 end |