author | wenzelm |
Sat, 14 Mar 2015 18:18:40 +0100 | |
changeset 59694 | d2bb4b5ed862 |
parent 59693 | d96cb03caf9e |
child 59735 | 24bee1b11fce |
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 |
|
48874
ff9cd47be39b
refined Thy_Load.check_thy: find more uses in body text, based on keywords;
wenzelm
parents:
48864
diff
changeset
|
9 |
type keywords = (string * Keyword.spec option) 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 |
58928
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58924
diff
changeset
|
15 |
val bootstrap_keywords: Keyword.keywords |
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58924
diff
changeset
|
16 |
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
|
17 |
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
|
18 |
val get_keywords': Proof.context -> Keyword.keywords |
46938
cda018294515
some support for outer syntax keyword declarations within theory header;
wenzelm
parents:
46737
diff
changeset
|
19 |
val args: header parser |
cda018294515
some support for outer syntax keyword declarations within theory header;
wenzelm
parents:
46737
diff
changeset
|
20 |
val read: Position.T -> string -> header |
48927
ef462b5558eb
theory def/ref position reports, which enable hyperlinks etc.;
wenzelm
parents:
48881
diff
changeset
|
21 |
val read_tokens: Token.T list -> header |
22106 | 22 |
end; |
23 |
||
32466 | 24 |
structure Thy_Header: THY_HEADER = |
22106 | 25 |
struct |
26 |
||
58928
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58924
diff
changeset
|
27 |
(** keyword declarations **) |
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58924
diff
changeset
|
28 |
|
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58924
diff
changeset
|
29 |
(* header *) |
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58924
diff
changeset
|
30 |
|
48874
ff9cd47be39b
refined Thy_Load.check_thy: find more uses in body text, based on keywords;
wenzelm
parents:
48864
diff
changeset
|
31 |
type keywords = (string * Keyword.spec option) list; |
ff9cd47be39b
refined Thy_Load.check_thy: find more uses in body text, based on keywords;
wenzelm
parents:
48864
diff
changeset
|
32 |
|
46938
cda018294515
some support for outer syntax keyword declarations within theory header;
wenzelm
parents:
46737
diff
changeset
|
33 |
type header = |
48927
ef462b5558eb
theory def/ref position reports, which enable hyperlinks etc.;
wenzelm
parents:
48881
diff
changeset
|
34 |
{name: string * Position.T, |
ef462b5558eb
theory def/ref position reports, which enable hyperlinks etc.;
wenzelm
parents:
48881
diff
changeset
|
35 |
imports: (string * Position.T) list, |
51294
0850d43cb355
discontinued obsolete header "files" -- these are loaded explicitly after exploring dependencies;
wenzelm
parents:
51293
diff
changeset
|
36 |
keywords: keywords}; |
46938
cda018294515
some support for outer syntax keyword declarations within theory header;
wenzelm
parents:
46737
diff
changeset
|
37 |
|
51294
0850d43cb355
discontinued obsolete header "files" -- these are loaded explicitly after exploring dependencies;
wenzelm
parents:
51293
diff
changeset
|
38 |
fun make name imports keywords : header = |
0850d43cb355
discontinued obsolete header "files" -- these are loaded explicitly after exploring dependencies;
wenzelm
parents:
51293
diff
changeset
|
39 |
{name = name, imports = imports, keywords = keywords}; |
46938
cda018294515
some support for outer syntax keyword declarations within theory header;
wenzelm
parents:
46737
diff
changeset
|
40 |
|
cda018294515
some support for outer syntax keyword declarations within theory header;
wenzelm
parents:
46737
diff
changeset
|
41 |
|
58928
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58924
diff
changeset
|
42 |
(* bootstrap keywords *) |
22106 | 43 |
|
44 |
val headerN = "header"; |
|
58868
c5e1cce7ace3
uniform heading commands work in any context, even in theory header;
wenzelm
parents:
58864
diff
changeset
|
45 |
val chapterN = "chapter"; |
c5e1cce7ace3
uniform heading commands work in any context, even in theory header;
wenzelm
parents:
58864
diff
changeset
|
46 |
val sectionN = "section"; |
c5e1cce7ace3
uniform heading commands work in any context, even in theory header;
wenzelm
parents:
58864
diff
changeset
|
47 |
val subsectionN = "subsection"; |
c5e1cce7ace3
uniform heading commands work in any context, even in theory header;
wenzelm
parents:
58864
diff
changeset
|
48 |
val subsubsectionN = "subsubsection"; |
58999
ed09ae4ea2d8
uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
wenzelm
parents:
58932
diff
changeset
|
49 |
val textN = "text"; |
ed09ae4ea2d8
uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
wenzelm
parents:
58932
diff
changeset
|
50 |
val txtN = "txt"; |
ed09ae4ea2d8
uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
wenzelm
parents:
58932
diff
changeset
|
51 |
val text_rawN = "text_raw"; |
58868
c5e1cce7ace3
uniform heading commands work in any context, even in theory header;
wenzelm
parents:
58864
diff
changeset
|
52 |
|
22106 | 53 |
val theoryN = "theory"; |
54 |
val importsN = "imports"; |
|
46938
cda018294515
some support for outer syntax keyword declarations within theory header;
wenzelm
parents:
46737
diff
changeset
|
55 |
val keywordsN = "keywords"; |
22106 | 56 |
val beginN = "begin"; |
57 |
||
58928
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58924
diff
changeset
|
58 |
val bootstrap_keywords = |
58903 | 59 |
Keyword.empty_keywords |
58928
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58924
diff
changeset
|
60 |
|> Keyword.add_keywords |
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58924
diff
changeset
|
61 |
[("%", NONE), |
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58924
diff
changeset
|
62 |
("(", NONE), |
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58924
diff
changeset
|
63 |
(")", NONE), |
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58924
diff
changeset
|
64 |
(",", NONE), |
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58924
diff
changeset
|
65 |
("::", NONE), |
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58924
diff
changeset
|
66 |
("==", NONE), |
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58924
diff
changeset
|
67 |
("and", NONE), |
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58924
diff
changeset
|
68 |
(beginN, NONE), |
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58924
diff
changeset
|
69 |
(importsN, NONE), |
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58924
diff
changeset
|
70 |
(keywordsN, NONE), |
58999
ed09ae4ea2d8
uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
wenzelm
parents:
58932
diff
changeset
|
71 |
(headerN, SOME ((Keyword.document_heading, []), [])), |
ed09ae4ea2d8
uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
wenzelm
parents:
58932
diff
changeset
|
72 |
(chapterN, SOME ((Keyword.document_heading, []), [])), |
ed09ae4ea2d8
uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
wenzelm
parents:
58932
diff
changeset
|
73 |
(sectionN, SOME ((Keyword.document_heading, []), [])), |
ed09ae4ea2d8
uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
wenzelm
parents:
58932
diff
changeset
|
74 |
(subsectionN, SOME ((Keyword.document_heading, []), [])), |
ed09ae4ea2d8
uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
wenzelm
parents:
58932
diff
changeset
|
75 |
(subsubsectionN, SOME ((Keyword.document_heading, []), [])), |
ed09ae4ea2d8
uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
wenzelm
parents:
58932
diff
changeset
|
76 |
(textN, SOME ((Keyword.document_body, []), [])), |
ed09ae4ea2d8
uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
wenzelm
parents:
58932
diff
changeset
|
77 |
(txtN, SOME ((Keyword.document_body, []), [])), |
ed09ae4ea2d8
uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
wenzelm
parents:
58932
diff
changeset
|
78 |
(text_rawN, SOME ((Keyword.document_raw, []), [])), |
58928
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58924
diff
changeset
|
79 |
(theoryN, SOME ((Keyword.thy_begin, []), ["theory"])), |
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58924
diff
changeset
|
80 |
("ML_file", SOME ((Keyword.thy_load, []), ["ML"]))]; |
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58924
diff
changeset
|
81 |
|
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58924
diff
changeset
|
82 |
|
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58924
diff
changeset
|
83 |
(* theory data *) |
22106 | 84 |
|
58928
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58924
diff
changeset
|
85 |
structure Data = Theory_Data |
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58924
diff
changeset
|
86 |
( |
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58924
diff
changeset
|
87 |
type T = Keyword.keywords; |
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58924
diff
changeset
|
88 |
val empty = bootstrap_keywords; |
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58924
diff
changeset
|
89 |
val extend = I; |
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58924
diff
changeset
|
90 |
val merge = Keyword.merge_keywords; |
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 |
|
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58924
diff
changeset
|
93 |
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
|
94 |
|
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58924
diff
changeset
|
95 |
val get_keywords = Data.get; |
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58924
diff
changeset
|
96 |
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
|
97 |
|
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58924
diff
changeset
|
98 |
|
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 |
(** concrete syntax **) |
22106 | 101 |
|
102 |
(* header args *) |
|
103 |
||
46938
cda018294515
some support for outer syntax keyword declarations within theory header;
wenzelm
parents:
46737
diff
changeset
|
104 |
local |
cda018294515
some support for outer syntax keyword declarations within theory header;
wenzelm
parents:
46737
diff
changeset
|
105 |
|
59694 | 106 |
fun imports name = |
107 |
if name = Context.PureN then Scan.succeed [] |
|
108 |
else Parse.$$$ importsN |-- Parse.!!! (Scan.repeat1 (Parse.position Parse.theory_xname)); |
|
53962
65bca53daf70
more robust parser: 'imports' are mandatory except for bootstrapping Pure;
wenzelm
parents:
51627
diff
changeset
|
109 |
|
48864
3ee314ae1e0a
added keyword kind "thy_load" (with optional list of file extensions);
wenzelm
parents:
48707
diff
changeset
|
110 |
val opt_files = |
3ee314ae1e0a
added keyword kind "thy_load" (with optional list of file extensions);
wenzelm
parents:
48707
diff
changeset
|
111 |
Scan.optional (Parse.$$$ "(" |-- Parse.!!! (Parse.list1 Parse.name) --| Parse.$$$ ")") []; |
50128
599c935aac82
alternative completion for outer syntax keywords;
wenzelm
parents:
48992
diff
changeset
|
112 |
|
48864
3ee314ae1e0a
added keyword kind "thy_load" (with optional list of file extensions);
wenzelm
parents:
48707
diff
changeset
|
113 |
val keyword_spec = |
3ee314ae1e0a
added keyword kind "thy_load" (with optional list of file extensions);
wenzelm
parents:
48707
diff
changeset
|
114 |
Parse.group (fn () => "outer syntax keyword specification") |
3ee314ae1e0a
added keyword kind "thy_load" (with optional list of file extensions);
wenzelm
parents:
48707
diff
changeset
|
115 |
(Parse.name -- opt_files -- Parse.tags); |
3ee314ae1e0a
added keyword kind "thy_load" (with optional list of file extensions);
wenzelm
parents:
48707
diff
changeset
|
116 |
|
50128
599c935aac82
alternative completion for outer syntax keywords;
wenzelm
parents:
48992
diff
changeset
|
117 |
val keyword_compl = |
599c935aac82
alternative completion for outer syntax keywords;
wenzelm
parents:
48992
diff
changeset
|
118 |
Parse.group (fn () => "outer syntax keyword completion") Parse.name; |
599c935aac82
alternative completion for outer syntax keywords;
wenzelm
parents:
48992
diff
changeset
|
119 |
|
46939 | 120 |
val keyword_decl = |
50128
599c935aac82
alternative completion for outer syntax keywords;
wenzelm
parents:
48992
diff
changeset
|
121 |
Scan.repeat1 Parse.string -- |
599c935aac82
alternative completion for outer syntax keywords;
wenzelm
parents:
48992
diff
changeset
|
122 |
Scan.option (Parse.$$$ "::" |-- Parse.!!! keyword_spec) -- |
599c935aac82
alternative completion for outer syntax keywords;
wenzelm
parents:
48992
diff
changeset
|
123 |
Scan.option (Parse.$$$ "==" |-- Parse.!!! keyword_compl) |
599c935aac82
alternative completion for outer syntax keywords;
wenzelm
parents:
48992
diff
changeset
|
124 |
>> (fn ((names, spec), _) => map (rpair spec) names); |
599c935aac82
alternative completion for outer syntax keywords;
wenzelm
parents:
48992
diff
changeset
|
125 |
|
46939 | 126 |
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
|
127 |
|
cda018294515
some support for outer syntax keyword declarations within theory header;
wenzelm
parents:
46737
diff
changeset
|
128 |
in |
22106 | 129 |
|
130 |
val args = |
|
59693 | 131 |
Parse.position Parse.theory_name :|-- (fn (name, pos) => |
59694 | 132 |
imports name -- |
53962
65bca53daf70
more robust parser: 'imports' are mandatory except for bootstrapping Pure;
wenzelm
parents:
51627
diff
changeset
|
133 |
Scan.optional (Parse.$$$ keywordsN |-- Parse.!!! keyword_decls) [] --| |
65bca53daf70
more robust parser: 'imports' are mandatory except for bootstrapping Pure;
wenzelm
parents:
51627
diff
changeset
|
134 |
Parse.$$$ beginN >> (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
|
135 |
|
cda018294515
some support for outer syntax keyword declarations within theory header;
wenzelm
parents:
46737
diff
changeset
|
136 |
end; |
22106 | 137 |
|
138 |
||
139 |
(* read header *) |
|
140 |
||
58868
c5e1cce7ace3
uniform heading commands work in any context, even in theory header;
wenzelm
parents:
58864
diff
changeset
|
141 |
val heading = |
58908 | 142 |
(Parse.command headerN || |
143 |
Parse.command chapterN || |
|
144 |
Parse.command sectionN || |
|
145 |
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
|
146 |
Parse.command subsubsectionN || |
ed09ae4ea2d8
uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
wenzelm
parents:
58932
diff
changeset
|
147 |
Parse.command textN || |
ed09ae4ea2d8
uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
wenzelm
parents:
58932
diff
changeset
|
148 |
Parse.command txtN || |
ed09ae4ea2d8
uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
wenzelm
parents:
58932
diff
changeset
|
149 |
Parse.command text_rawN) -- |
58868
c5e1cce7ace3
uniform heading commands work in any context, even in theory header;
wenzelm
parents:
58864
diff
changeset
|
150 |
Parse.tags -- Parse.!!! Parse.document_source; |
c5e1cce7ace3
uniform heading commands work in any context, even in theory header;
wenzelm
parents:
58864
diff
changeset
|
151 |
|
22106 | 152 |
val header = |
58908 | 153 |
(Scan.repeat heading -- Parse.command theoryN -- Parse.tags) |-- Parse.!!! args; |
22106 | 154 |
|
48927
ef462b5558eb
theory def/ref position reports, which enable hyperlinks etc.;
wenzelm
parents:
48881
diff
changeset
|
155 |
fun token_source pos str = |
ef462b5558eb
theory def/ref position reports, which enable hyperlinks etc.;
wenzelm
parents:
48881
diff
changeset
|
156 |
str |
ef462b5558eb
theory def/ref position reports, which enable hyperlinks etc.;
wenzelm
parents:
48881
diff
changeset
|
157 |
|> Source.of_string_limited 8000 |
ef462b5558eb
theory def/ref position reports, which enable hyperlinks etc.;
wenzelm
parents:
48881
diff
changeset
|
158 |
|> Symbol.source |
58928
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58924
diff
changeset
|
159 |
|> Token.source_strict bootstrap_keywords pos; |
48927
ef462b5558eb
theory def/ref position reports, which enable hyperlinks etc.;
wenzelm
parents:
48881
diff
changeset
|
160 |
|
ef462b5558eb
theory def/ref position reports, which enable hyperlinks etc.;
wenzelm
parents:
48881
diff
changeset
|
161 |
fun read_source pos source = |
22106 | 162 |
let val res = |
48927
ef462b5558eb
theory def/ref position reports, which enable hyperlinks etc.;
wenzelm
parents:
48881
diff
changeset
|
163 |
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
|
164 |
|> Token.source_proper |
58864 | 165 |
|> Source.source Token.stopper (Scan.single (Scan.error (Parse.!!! header))) |
22106 | 166 |
|> Source.get_single; |
167 |
in |
|
42003
6e45dc518ebb
replaced File.check by specific File.check_file, File.check_dir;
wenzelm
parents:
41944
diff
changeset
|
168 |
(case res of |
46938
cda018294515
some support for outer syntax keyword declarations within theory header;
wenzelm
parents:
46737
diff
changeset
|
169 |
SOME (h, _) => h |
48992 | 170 |
| NONE => error ("Unexpected end of input" ^ Position.here pos)) |
22106 | 171 |
end; |
172 |
||
48927
ef462b5558eb
theory def/ref position reports, which enable hyperlinks etc.;
wenzelm
parents:
48881
diff
changeset
|
173 |
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
|
174 |
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
|
175 |
|
22106 | 176 |
end; |