author | wenzelm |
Thu, 01 Jun 2017 21:43:36 +0200 | |
changeset 65999 | ee4cf96a9406 |
parent 65452 | 9e9750a7932c |
child 66771 | 925d10a7a610 |
permissions | -rw-r--r-- |
22106 | 1 |
(* Title: Pure/Thy/thy_header.ML |
46939 | 2 |
Author: Makarius |
22106 | 3 |
|
46939 | 4 |
Static theory header information. |
22106 | 5 |
*) |
6 |
||
7 |
signature THY_HEADER = |
|
8 |
sig |
|
63429 | 9 |
type keywords = ((string * Position.T) * Keyword.spec) list |
46938
cda018294515
some support for outer syntax keyword declarations within theory header;
wenzelm
parents:
46737
diff
changeset
|
10 |
type header = |
48927
ef462b5558eb
theory def/ref position reports, which enable hyperlinks etc.;
wenzelm
parents:
48881
diff
changeset
|
11 |
{name: string * Position.T, |
ef462b5558eb
theory def/ref position reports, which enable hyperlinks etc.;
wenzelm
parents:
48881
diff
changeset
|
12 |
imports: (string * Position.T) list, |
51294
0850d43cb355
discontinued obsolete header "files" -- these are loaded explicitly after exploring dependencies;
wenzelm
parents:
51293
diff
changeset
|
13 |
keywords: keywords} |
0850d43cb355
discontinued obsolete header "files" -- these are loaded explicitly after exploring dependencies;
wenzelm
parents:
51293
diff
changeset
|
14 |
val make: string * Position.T -> (string * Position.T) list -> keywords -> header |
59735 | 15 |
val theoryN: string |
58928
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58924
diff
changeset
|
16 |
val bootstrap_keywords: Keyword.keywords |
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58924
diff
changeset
|
17 |
val add_keywords: keywords -> theory -> theory |
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58924
diff
changeset
|
18 |
val get_keywords: theory -> Keyword.keywords |
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58924
diff
changeset
|
19 |
val get_keywords': Proof.context -> Keyword.keywords |
62895
54c2abe7e9a4
treat ROOT.ML as theory with header "theory ML_Root imports ML_Bootstrap begin";
wenzelm
parents:
62849
diff
changeset
|
20 |
val ml_bootstrapN: string |
62932
db12de2367ca
support ROOT0.ML as well -- independently of ROOT.ML;
wenzelm
parents:
62895
diff
changeset
|
21 |
val ml_roots: string list |
63022 | 22 |
val bootstrap_thys: string list |
65452 | 23 |
val import_name: string -> string |
46938
cda018294515
some support for outer syntax keyword declarations within theory header;
wenzelm
parents:
46737
diff
changeset
|
24 |
val args: header parser |
cda018294515
some support for outer syntax keyword declarations within theory header;
wenzelm
parents:
46737
diff
changeset
|
25 |
val read: Position.T -> string -> header |
48927
ef462b5558eb
theory def/ref position reports, which enable hyperlinks etc.;
wenzelm
parents:
48881
diff
changeset
|
26 |
val read_tokens: Token.T list -> header |
22106 | 27 |
end; |
28 |
||
32466 | 29 |
structure Thy_Header: THY_HEADER = |
22106 | 30 |
struct |
31 |
||
58928
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58924
diff
changeset
|
32 |
(** keyword declarations **) |
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58924
diff
changeset
|
33 |
|
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58924
diff
changeset
|
34 |
(* header *) |
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58924
diff
changeset
|
35 |
|
63429 | 36 |
type keywords = ((string * Position.T) * Keyword.spec) list; |
48874
ff9cd47be39b
refined Thy_Load.check_thy: find more uses in body text, based on keywords;
wenzelm
parents:
48864
diff
changeset
|
37 |
|
46938
cda018294515
some support for outer syntax keyword declarations within theory header;
wenzelm
parents:
46737
diff
changeset
|
38 |
type header = |
48927
ef462b5558eb
theory def/ref position reports, which enable hyperlinks etc.;
wenzelm
parents:
48881
diff
changeset
|
39 |
{name: string * Position.T, |
ef462b5558eb
theory def/ref position reports, which enable hyperlinks etc.;
wenzelm
parents:
48881
diff
changeset
|
40 |
imports: (string * Position.T) list, |
51294
0850d43cb355
discontinued obsolete header "files" -- these are loaded explicitly after exploring dependencies;
wenzelm
parents:
51293
diff
changeset
|
41 |
keywords: keywords}; |
46938
cda018294515
some support for outer syntax keyword declarations within theory header;
wenzelm
parents:
46737
diff
changeset
|
42 |
|
51294
0850d43cb355
discontinued obsolete header "files" -- these are loaded explicitly after exploring dependencies;
wenzelm
parents:
51293
diff
changeset
|
43 |
fun make name imports keywords : header = |
0850d43cb355
discontinued obsolete header "files" -- these are loaded explicitly after exploring dependencies;
wenzelm
parents:
51293
diff
changeset
|
44 |
{name = name, imports = imports, keywords = keywords}; |
46938
cda018294515
some support for outer syntax keyword declarations within theory header;
wenzelm
parents:
46737
diff
changeset
|
45 |
|
cda018294515
some support for outer syntax keyword declarations within theory header;
wenzelm
parents:
46737
diff
changeset
|
46 |
|
58928
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58924
diff
changeset
|
47 |
(* bootstrap keywords *) |
22106 | 48 |
|
58868
c5e1cce7ace3
uniform heading commands work in any context, even in theory header;
wenzelm
parents:
58864
diff
changeset
|
49 |
val chapterN = "chapter"; |
c5e1cce7ace3
uniform heading commands work in any context, even in theory header;
wenzelm
parents:
58864
diff
changeset
|
50 |
val sectionN = "section"; |
c5e1cce7ace3
uniform heading commands work in any context, even in theory header;
wenzelm
parents:
58864
diff
changeset
|
51 |
val subsectionN = "subsection"; |
c5e1cce7ace3
uniform heading commands work in any context, even in theory header;
wenzelm
parents:
58864
diff
changeset
|
52 |
val subsubsectionN = "subsubsection"; |
61463 | 53 |
val paragraphN = "paragraph"; |
54 |
val subparagraphN = "subparagraph"; |
|
58999
ed09ae4ea2d8
uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
wenzelm
parents:
58932
diff
changeset
|
55 |
val textN = "text"; |
ed09ae4ea2d8
uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
wenzelm
parents:
58932
diff
changeset
|
56 |
val txtN = "txt"; |
ed09ae4ea2d8
uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
wenzelm
parents:
58932
diff
changeset
|
57 |
val text_rawN = "text_raw"; |
58868
c5e1cce7ace3
uniform heading commands work in any context, even in theory header;
wenzelm
parents:
58864
diff
changeset
|
58 |
|
22106 | 59 |
val theoryN = "theory"; |
60 |
val importsN = "imports"; |
|
46938
cda018294515
some support for outer syntax keyword declarations within theory header;
wenzelm
parents:
46737
diff
changeset
|
61 |
val keywordsN = "keywords"; |
63579 | 62 |
val abbrevsN = "abbrevs"; |
22106 | 63 |
val beginN = "begin"; |
64 |
||
58928
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58924
diff
changeset
|
65 |
val bootstrap_keywords = |
58903 | 66 |
Keyword.empty_keywords |
58928
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58924
diff
changeset
|
67 |
|> Keyword.add_keywords |
64556 | 68 |
[(("%", \<^here>), Keyword.no_spec), |
69 |
(("(", \<^here>), Keyword.no_spec), |
|
70 |
((")", \<^here>), Keyword.no_spec), |
|
71 |
((",", \<^here>), Keyword.no_spec), |
|
72 |
(("::", \<^here>), Keyword.no_spec), |
|
73 |
(("=", \<^here>), Keyword.no_spec), |
|
74 |
(("and", \<^here>), Keyword.no_spec), |
|
75 |
((beginN, \<^here>), Keyword.quasi_command_spec), |
|
76 |
((importsN, \<^here>), Keyword.quasi_command_spec), |
|
77 |
((keywordsN, \<^here>), Keyword.quasi_command_spec), |
|
78 |
((abbrevsN, \<^here>), Keyword.quasi_command_spec), |
|
79 |
((chapterN, \<^here>), ((Keyword.document_heading, []), [])), |
|
80 |
((sectionN, \<^here>), ((Keyword.document_heading, []), [])), |
|
81 |
((subsectionN, \<^here>), ((Keyword.document_heading, []), [])), |
|
82 |
((subsubsectionN, \<^here>), ((Keyword.document_heading, []), [])), |
|
83 |
((paragraphN, \<^here>), ((Keyword.document_heading, []), [])), |
|
84 |
((subparagraphN, \<^here>), ((Keyword.document_heading, []), [])), |
|
85 |
((textN, \<^here>), ((Keyword.document_body, []), [])), |
|
86 |
((txtN, \<^here>), ((Keyword.document_body, []), [])), |
|
87 |
((text_rawN, \<^here>), ((Keyword.document_raw, []), [])), |
|
88 |
((theoryN, \<^here>), ((Keyword.thy_begin, []), ["theory"])), |
|
89 |
(("ML", \<^here>), ((Keyword.thy_decl, []), ["ML"]))]; |
|
58928
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58924
diff
changeset
|
90 |
|
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58924
diff
changeset
|
91 |
|
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58924
diff
changeset
|
92 |
(* theory data *) |
22106 | 93 |
|
58928
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58924
diff
changeset
|
94 |
structure Data = Theory_Data |
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58924
diff
changeset
|
95 |
( |
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58924
diff
changeset
|
96 |
type T = Keyword.keywords; |
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58924
diff
changeset
|
97 |
val empty = bootstrap_keywords; |
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58924
diff
changeset
|
98 |
val extend = I; |
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58924
diff
changeset
|
99 |
val merge = Keyword.merge_keywords; |
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58924
diff
changeset
|
100 |
); |
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58924
diff
changeset
|
101 |
|
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58924
diff
changeset
|
102 |
val add_keywords = Data.map o Keyword.add_keywords; |
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58924
diff
changeset
|
103 |
|
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58924
diff
changeset
|
104 |
val get_keywords = Data.get; |
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58924
diff
changeset
|
105 |
val get_keywords' = get_keywords o Proof_Context.theory_of; |
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58924
diff
changeset
|
106 |
|
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58924
diff
changeset
|
107 |
|
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58924
diff
changeset
|
108 |
|
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58924
diff
changeset
|
109 |
(** concrete syntax **) |
22106 | 110 |
|
62895
54c2abe7e9a4
treat ROOT.ML as theory with header "theory ML_Root imports ML_Bootstrap begin";
wenzelm
parents:
62849
diff
changeset
|
111 |
(* names *) |
54c2abe7e9a4
treat ROOT.ML as theory with header "theory ML_Root imports ML_Bootstrap begin";
wenzelm
parents:
62849
diff
changeset
|
112 |
|
54c2abe7e9a4
treat ROOT.ML as theory with header "theory ML_Root imports ML_Bootstrap begin";
wenzelm
parents:
62849
diff
changeset
|
113 |
val ml_bootstrapN = "ML_Bootstrap"; |
62932
db12de2367ca
support ROOT0.ML as well -- independently of ROOT.ML;
wenzelm
parents:
62895
diff
changeset
|
114 |
val ml_roots = ["ML_Root0", "ML_Root"]; |
63022 | 115 |
val bootstrap_thys = ["Bootstrap_Pure", "Bootstrap_ML_Bootstrap"]; |
62932
db12de2367ca
support ROOT0.ML as well -- independently of ROOT.ML;
wenzelm
parents:
62895
diff
changeset
|
116 |
|
65999 | 117 |
val import_name = Path.base_name o Path.explode; |
62895
54c2abe7e9a4
treat ROOT.ML as theory with header "theory ML_Root imports ML_Bootstrap begin";
wenzelm
parents:
62849
diff
changeset
|
118 |
|
54c2abe7e9a4
treat ROOT.ML as theory with header "theory ML_Root imports ML_Bootstrap begin";
wenzelm
parents:
62849
diff
changeset
|
119 |
|
22106 | 120 |
(* header args *) |
121 |
||
46938
cda018294515
some support for outer syntax keyword declarations within theory header;
wenzelm
parents:
46737
diff
changeset
|
122 |
local |
cda018294515
some support for outer syntax keyword declarations within theory header;
wenzelm
parents:
46737
diff
changeset
|
123 |
|
59694 | 124 |
fun imports name = |
125 |
if name = Context.PureN then Scan.succeed [] |
|
62969 | 126 |
else Parse.$$$ importsN |-- Parse.!!! (Scan.repeat1 (Parse.position Parse.theory_name)); |
53962
65bca53daf70
more robust parser: 'imports' are mandatory except for bootstrapping Pure;
wenzelm
parents:
51627
diff
changeset
|
127 |
|
48864
3ee314ae1e0a
added keyword kind "thy_load" (with optional list of file extensions);
wenzelm
parents:
48707
diff
changeset
|
128 |
val opt_files = |
3ee314ae1e0a
added keyword kind "thy_load" (with optional list of file extensions);
wenzelm
parents:
48707
diff
changeset
|
129 |
Scan.optional (Parse.$$$ "(" |-- Parse.!!! (Parse.list1 Parse.name) --| Parse.$$$ ")") []; |
50128
599c935aac82
alternative completion for outer syntax keywords;
wenzelm
parents:
48992
diff
changeset
|
130 |
|
48864
3ee314ae1e0a
added keyword kind "thy_load" (with optional list of file extensions);
wenzelm
parents:
48707
diff
changeset
|
131 |
val keyword_spec = |
3ee314ae1e0a
added keyword kind "thy_load" (with optional list of file extensions);
wenzelm
parents:
48707
diff
changeset
|
132 |
Parse.group (fn () => "outer syntax keyword specification") |
3ee314ae1e0a
added keyword kind "thy_load" (with optional list of file extensions);
wenzelm
parents:
48707
diff
changeset
|
133 |
(Parse.name -- opt_files -- Parse.tags); |
3ee314ae1e0a
added keyword kind "thy_load" (with optional list of file extensions);
wenzelm
parents:
48707
diff
changeset
|
134 |
|
46939 | 135 |
val keyword_decl = |
59934
b65c4370f831
more position information and PIDE markup for command keywords;
wenzelm
parents:
59735
diff
changeset
|
136 |
Scan.repeat1 (Parse.position Parse.string) -- |
63579 | 137 |
Scan.optional (Parse.$$$ "::" |-- Parse.!!! keyword_spec) Keyword.no_spec |
138 |
>> (fn (names, spec) => map (rpair spec) names); |
|
139 |
||
140 |
val abbrevs = Scan.repeat1 (Parse.text -- (Parse.$$$ "=" |-- Parse.!!! Parse.text)); |
|
50128
599c935aac82
alternative completion for outer syntax keywords;
wenzelm
parents:
48992
diff
changeset
|
141 |
|
46939 | 142 |
val keyword_decls = Parse.and_list1 keyword_decl >> flat; |
46938
cda018294515
some support for outer syntax keyword declarations within theory header;
wenzelm
parents:
46737
diff
changeset
|
143 |
|
cda018294515
some support for outer syntax keyword declarations within theory header;
wenzelm
parents:
46737
diff
changeset
|
144 |
in |
22106 | 145 |
|
146 |
val args = |
|
59693 | 147 |
Parse.position Parse.theory_name :|-- (fn (name, pos) => |
59694 | 148 |
imports name -- |
53962
65bca53daf70
more robust parser: 'imports' are mandatory except for bootstrapping Pure;
wenzelm
parents:
51627
diff
changeset
|
149 |
Scan.optional (Parse.$$$ keywordsN |-- Parse.!!! keyword_decls) [] --| |
63579 | 150 |
(Scan.optional (Parse.$$$ abbrevsN |-- Parse.!!! abbrevs) [] -- Parse.$$$ beginN) |
151 |
>> (fn (imports, keywords) => make (name, pos) imports keywords)); |
|
46938
cda018294515
some support for outer syntax keyword declarations within theory header;
wenzelm
parents:
46737
diff
changeset
|
152 |
|
cda018294515
some support for outer syntax keyword declarations within theory header;
wenzelm
parents:
46737
diff
changeset
|
153 |
end; |
22106 | 154 |
|
155 |
||
156 |
(* read header *) |
|
157 |
||
58868
c5e1cce7ace3
uniform heading commands work in any context, even in theory header;
wenzelm
parents:
58864
diff
changeset
|
158 |
val heading = |
62453 | 159 |
(Parse.command chapterN || |
58908 | 160 |
Parse.command sectionN || |
161 |
Parse.command subsectionN || |
|
58999
ed09ae4ea2d8
uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
wenzelm
parents:
58932
diff
changeset
|
162 |
Parse.command subsubsectionN || |
61463 | 163 |
Parse.command paragraphN || |
164 |
Parse.command subparagraphN || |
|
58999
ed09ae4ea2d8
uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
wenzelm
parents:
58932
diff
changeset
|
165 |
Parse.command textN || |
ed09ae4ea2d8
uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
wenzelm
parents:
58932
diff
changeset
|
166 |
Parse.command txtN || |
ed09ae4ea2d8
uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
wenzelm
parents:
58932
diff
changeset
|
167 |
Parse.command text_rawN) -- |
58868
c5e1cce7ace3
uniform heading commands work in any context, even in theory header;
wenzelm
parents:
58864
diff
changeset
|
168 |
Parse.tags -- Parse.!!! Parse.document_source; |
c5e1cce7ace3
uniform heading commands work in any context, even in theory header;
wenzelm
parents:
58864
diff
changeset
|
169 |
|
22106 | 170 |
val header = |
58908 | 171 |
(Scan.repeat heading -- Parse.command theoryN -- Parse.tags) |-- Parse.!!! args; |
22106 | 172 |
|
63936 | 173 |
fun token_source pos = |
174 |
Symbol.explode |
|
175 |
#> Source.of_list |
|
176 |
#> Token.source_strict bootstrap_keywords pos; |
|
48927
ef462b5558eb
theory def/ref position reports, which enable hyperlinks etc.;
wenzelm
parents:
48881
diff
changeset
|
177 |
|
ef462b5558eb
theory def/ref position reports, which enable hyperlinks etc.;
wenzelm
parents:
48881
diff
changeset
|
178 |
fun read_source pos source = |
22106 | 179 |
let val res = |
48927
ef462b5558eb
theory def/ref position reports, which enable hyperlinks etc.;
wenzelm
parents:
48881
diff
changeset
|
180 |
source |
36959
f5417836dbea
renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents:
36950
diff
changeset
|
181 |
|> Token.source_proper |
58864 | 182 |
|> Source.source Token.stopper (Scan.single (Scan.error (Parse.!!! header))) |
22106 | 183 |
|> Source.get_single; |
184 |
in |
|
42003
6e45dc518ebb
replaced File.check by specific File.check_file, File.check_dir;
wenzelm
parents:
41944
diff
changeset
|
185 |
(case res of |
46938
cda018294515
some support for outer syntax keyword declarations within theory header;
wenzelm
parents:
46737
diff
changeset
|
186 |
SOME (h, _) => h |
48992 | 187 |
| NONE => error ("Unexpected end of input" ^ Position.here pos)) |
22106 | 188 |
end; |
189 |
||
48927
ef462b5558eb
theory def/ref position reports, which enable hyperlinks etc.;
wenzelm
parents:
48881
diff
changeset
|
190 |
fun read pos str = read_source pos (token_source pos str); |
ef462b5558eb
theory def/ref position reports, which enable hyperlinks etc.;
wenzelm
parents:
48881
diff
changeset
|
191 |
fun read_tokens toks = read_source Position.none (Source.of_list toks); |
ef462b5558eb
theory def/ref position reports, which enable hyperlinks etc.;
wenzelm
parents:
48881
diff
changeset
|
192 |
|
22106 | 193 |
end; |