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