23
|
1 |
theory Base
|
|
2 |
imports Main
|
|
3 |
uses
|
57
|
4 |
"chunks.ML"
|
23
|
5 |
"antiquote_setup.ML"
|
|
6 |
begin
|
|
7 |
|
64
9a6e5e0c4906
deleted old files and added code to give a special tag to the command ML
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
8 |
(* to have a special tag for text enclosed in ML *)
|
9a6e5e0c4906
deleted old files and added code to give a special tag to the command ML
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
9 |
ML {*
|
9a6e5e0c4906
deleted old files and added code to give a special tag to the command ML
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
10 |
|
9a6e5e0c4906
deleted old files and added code to give a special tag to the command ML
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
11 |
val _ =
|
9a6e5e0c4906
deleted old files and added code to give a special tag to the command ML
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
12 |
OuterSyntax.command "ML" "eval ML text within theory"
|
106
bdd82350cf22
renamed in the pdf all instances of cookbook to tutorial (in order to sound more serious)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
13 |
(OuterKeyword.tag "TutorialML" OuterKeyword.thy_decl)
|
64
9a6e5e0c4906
deleted old files and added code to give a special tag to the command ML
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
14 |
(OuterParse.ML_source >> (fn (txt, pos) =>
|
9a6e5e0c4906
deleted old files and added code to give a special tag to the command ML
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
15 |
Toplevel.generic_theory (ML_Context.exec (fn () => ML_Context.eval true pos txt))));
|
9a6e5e0c4906
deleted old files and added code to give a special tag to the command ML
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
16 |
*}
|
9a6e5e0c4906
deleted old files and added code to give a special tag to the command ML
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
17 |
|
80
|
18 |
|
23
|
19 |
end
|