author | wenzelm |
Fri, 31 Oct 2014 21:35:11 +0100 | |
changeset 58852 | 621c052789b4 |
parent 58842 | 22b87ab47d3b |
child 58918 | 8d36bc5eaed3 |
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 |
||
10 |
val _ = |
|
11 |
Outer_Syntax.command |
|
56204 | 12 |
(("theory", Keyword.tag_theory Keyword.thy_begin), @{here}) "begin theory" |
58852 | 13 |
(Thy_Header.args >> |
14 |
(fn _ => Toplevel.init_theory (fn () => error "Missing theory initialization"))); |
|
48879 | 15 |
|
16 |
val _ = |
|
17 |
Outer_Syntax.command |
|
56204 | 18 |
(("ML_file", Keyword.tag_ml Keyword.thy_load), @{here}) "ML text from file" |
56208 | 19 |
(Resources.parse_files "ML_file" >> (fn files => Toplevel.generic_theory (fn gthy => |
48879 | 20 |
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
|
21 |
val [{src_path, lines, digest, pos}] = files (Context.theory_of gthy); |
56208 | 22 |
val provide = Resources.provide (src_path, digest); |
55828
42ac3cfb89f6
clarified language markup: added "delimited" property;
wenzelm
parents:
55788
diff
changeset
|
23 |
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
|
24 |
val flags = {SML = false, exchange = false, redirect = true, verbose = true}; |
48879 | 25 |
in |
26 |
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
|
27 |
|> ML_Context.exec (fn () => ML_Context.eval_source flags source) |
48879 | 28 |
|> Local_Theory.propagate_ml_env |
29 |
|> Context.mapping provide (Local_Theory.background_theory provide) |
|
30 |
end))); |
|
31 |
||
32 |
end; |
|
33 |