7 structure Pure_Syn: sig end = |
7 structure Pure_Syn: sig end = |
8 struct |
8 struct |
9 |
9 |
10 val _ = |
10 val _ = |
11 Outer_Syntax.command |
11 Outer_Syntax.command |
12 (("theory", Keyword.tag_theory Keyword.thy_begin), Position.file "pure_syn.ML") |
12 (("theory", Keyword.tag_theory Keyword.thy_begin), @{here}) "begin theory" |
13 "begin theory context" |
|
14 (Thy_Header.args >> (fn header => |
13 (Thy_Header.args >> (fn header => |
15 Toplevel.print o |
14 Toplevel.print o |
16 Toplevel.init_theory |
15 Toplevel.init_theory |
17 (fn () => Thy_Info.toplevel_begin_theory (! ProofGeneral.master_path) header))); |
16 (fn () => Thy_Info.toplevel_begin_theory (! ProofGeneral.master_path) header))); |
18 |
17 |
19 val _ = |
18 val _ = |
20 Outer_Syntax.command |
19 Outer_Syntax.command |
21 (("ML_file", Keyword.tag_ml Keyword.thy_load), Position.file "pure_syn.ML") |
20 (("ML_file", Keyword.tag_ml Keyword.thy_load), @{here}) "ML text from file" |
22 "ML text from file" |
|
23 (Thy_Load.parse_files "ML_file" >> (fn files => Toplevel.generic_theory (fn gthy => |
21 (Thy_Load.parse_files "ML_file" >> (fn files => Toplevel.generic_theory (fn gthy => |
24 let |
22 let |
25 val [{src_path, lines, digest, pos}] = files (Context.theory_of gthy); |
23 val [{src_path, lines, digest, pos}] = files (Context.theory_of gthy); |
26 val provide = Thy_Load.provide (src_path, digest); |
24 val provide = Thy_Load.provide (src_path, digest); |
27 val source = {delimited = true, text = cat_lines lines, pos = pos}; |
25 val source = {delimited = true, text = cat_lines lines, pos = pos}; |