author | wenzelm |
Wed, 22 Aug 2012 12:47:49 +0200 | |
changeset 48881 | 46e053eda5dd |
parent 48879 | cb5cdbb645cd |
child 48896 | bb1f461a7815 |
permissions | -rw-r--r-- |
48879 | 1 |
(* Title: Pure/pure_syn.ML |
2 |
Author: Makarius |
|
3 |
||
4 |
Minimal outer syntax for bootstrapping Pure. |
|
5 |
*) |
|
6 |
||
7 |
structure Pure_Syn: sig end = |
|
8 |
struct |
|
9 |
||
10 |
val _ = |
|
11 |
Outer_Syntax.command |
|
12 |
(("theory", Keyword.tag_theory Keyword.thy_begin), Position.none) "begin theory context" |
|
13 |
(Thy_Header.args >> (fn header => |
|
14 |
Toplevel.print o |
|
15 |
Toplevel.init_theory |
|
16 |
(fn () => Thy_Info.toplevel_begin_theory (Thy_Load.get_master_path ()) header))); |
|
17 |
||
18 |
val _ = |
|
19 |
Outer_Syntax.command |
|
20 |
(("ML_file", Keyword.tag_ml Keyword.thy_load), Position.none) "ML text from file" |
|
21 |
(Scan.ahead Parse.path -- Thy_Load.parse_files "ML_file" |
|
48881
46e053eda5dd
clarified Parse.path vs. Parse.explode -- prefer errors in proper transaction context;
wenzelm
parents:
48879
diff
changeset
|
22 |
>> (fn (name, files) => Toplevel.generic_theory (fn gthy => |
48879 | 23 |
let |
48881
46e053eda5dd
clarified Parse.path vs. Parse.explode -- prefer errors in proper transaction context;
wenzelm
parents:
48879
diff
changeset
|
24 |
val src_path = Path.explode name; |
48879 | 25 |
val (dir, [(txt, pos)]) = files (Context.theory_of gthy); |
26 |
val provide = Thy_Load.provide (src_path, (File.full_path dir src_path, SHA1.digest txt)); |
|
27 |
in |
|
28 |
gthy |
|
29 |
|> ML_Context.exec (fn () => ML_Context.eval_text true pos txt) |
|
30 |
|> Local_Theory.propagate_ml_env |
|
31 |
|> Context.mapping provide (Local_Theory.background_theory provide) |
|
32 |
end))); |
|
33 |
||
34 |
end; |
|
35 |