author | wenzelm |
Thu, 06 Nov 2014 11:44:41 +0100 | |
changeset 58918 | 8d36bc5eaed3 |
parent 58852 | 621c052789b4 |
child 58928 | 23d0ffd48006 |
permissions | -rw-r--r-- |
48879 | 1 |
(* Title: Pure/pure_syn.ML |
2 |
Author: Makarius |
|
3 |
||
52546 | 4 |
Minimal outer syntax for bootstrapping Isabelle/Pure. |
48879 | 5 |
*) |
6 |
||
7 |
structure Pure_Syn: sig end = |
|
8 |
struct |
|
9 |
||
58918 | 10 |
(* keywords *) |
11 |
||
12 |
val keywords: Thy_Header.keywords = |
|
13 |
[("theory", SOME (("thy_begin", []), ["theory"])), |
|
14 |
("ML_file", SOME (("thy_load", []), ["ML"]))]; |
|
15 |
||
16 |
fun command_spec (name, pos) = |
|
17 |
(case AList.lookup (op =) keywords name of |
|
18 |
SOME (SOME spec) => Keyword.command_spec ((name, spec), pos) |
|
19 |
| _ => error ("Bad command specification " ^ quote name ^ Position.here pos)); |
|
20 |
||
21 |
val _ = Thy_Header.define_keywords keywords; |
|
22 |
val _ = Theory.setup (fold Thy_Header.declare_keyword keywords); |
|
23 |
||
24 |
||
25 |
(* commands *) |
|
26 |
||
48879 | 27 |
val _ = |
28 |
Outer_Syntax.command |
|
58918 | 29 |
(command_spec ("theory", @{here})) "begin theory" |
58852 | 30 |
(Thy_Header.args >> |
31 |
(fn _ => Toplevel.init_theory (fn () => error "Missing theory initialization"))); |
|
48879 | 32 |
|
33 |
val _ = |
|
34 |
Outer_Syntax.command |
|
58918 | 35 |
(command_spec ("ML_file", @{here})) "ML text from file" |
56208 | 36 |
(Resources.parse_files "ML_file" >> (fn files => Toplevel.generic_theory (fn gthy => |
48879 | 37 |
let |
55788
67699e08e969
store blobs / inlined files as separate text lines: smaller values are more healthy for the Poly/ML RTS and allow implicit sharing;
wenzelm
parents:
54450
diff
changeset
|
38 |
val [{src_path, lines, digest, pos}] = files (Context.theory_of gthy); |
56208 | 39 |
val provide = Resources.provide (src_path, digest); |
55828
42ac3cfb89f6
clarified language markup: added "delimited" property;
wenzelm
parents:
55788
diff
changeset
|
40 |
val source = {delimited = true, text = cat_lines lines, pos = pos}; |
56618
874bdedb2313
added command 'SML_export' and 'SML_import' for exchange of toplevel bindings;
wenzelm
parents:
56304
diff
changeset
|
41 |
val flags = {SML = false, exchange = false, redirect = true, verbose = true}; |
48879 | 42 |
in |
43 |
gthy |
|
56304
40274e4f5ebf
redirect ML_Compiler reports more directly: only the (big) parse tree report is deferred via Execution.print (NB: this does not work for asynchronous "diag" commands);
wenzelm
parents:
56275
diff
changeset
|
44 |
|> ML_Context.exec (fn () => ML_Context.eval_source flags source) |
48879 | 45 |
|> Local_Theory.propagate_ml_env |
46 |
|> Context.mapping provide (Local_Theory.background_theory provide) |
|
47 |
end))); |
|
48 |
||
49 |
end; |
|
50 |