| changeset 64 | 9a6e5e0c4906 |
| parent 57 | 065f472c09ab |
| child 80 | 95e9c4556221 |
| 63:83cea5dc6bac | 64:9a6e5e0c4906 |
|---|---|
3 uses |
3 uses |
4 "chunks.ML" |
4 "chunks.ML" |
5 "antiquote_setup.ML" |
5 "antiquote_setup.ML" |
6 begin |
6 begin |
7 |
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 "CookBookML" 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 |
|
8 end |
18 end |