author | wenzelm |
Mon, 17 May 2010 15:11:25 +0200 | |
changeset 36959 | f5417836dbea |
parent 36950 | 75b8f26f2f07 |
child 37950 | bc285d91041e |
permissions | -rw-r--r-- |
22106 | 1 |
(* Title: Pure/Thy/thy_header.ML |
2 |
Author: Markus Wenzel, TU Muenchen |
|
3 |
||
4 |
Theory headers -- independent of outer syntax. |
|
5 |
*) |
|
6 |
||
7 |
signature THY_HEADER = |
|
8 |
sig |
|
36959
f5417836dbea
renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents:
36950
diff
changeset
|
9 |
val args: Token.T list -> (string * string list * (string * bool) list) * Token.T list |
23863 | 10 |
val read: Position.T -> (string, 'a) Source.source -> string * string list * (string * bool) list |
22106 | 11 |
end; |
12 |
||
32466 | 13 |
structure Thy_Header: THY_HEADER = |
22106 | 14 |
struct |
15 |
||
16 |
(* keywords *) |
|
17 |
||
18 |
val headerN = "header"; |
|
19 |
val theoryN = "theory"; |
|
20 |
val importsN = "imports"; |
|
21 |
val usesN = "uses"; |
|
22 |
val beginN = "begin"; |
|
23 |
||
24577 | 24 |
val header_lexicon = Scan.make_lexicon |
25 |
(map Symbol.explode ["%", "(", ")", ";", beginN, headerN, importsN, theoryN, usesN]); |
|
22106 | 26 |
|
27 |
||
28 |
(* header args *) |
|
29 |
||
36950 | 30 |
val file_name = Parse.group "file name" Parse.name; |
31 |
val theory_name = Parse.group "theory name" Parse.name; |
|
27890
62ac62e30ab1
args: explicit groups for file_name, theory_name;
wenzelm
parents:
27872
diff
changeset
|
32 |
|
36950 | 33 |
val file = |
34 |
Parse.$$$ "(" |-- Parse.!!! (file_name --| Parse.$$$ ")") >> rpair false || |
|
35 |
file_name >> rpair true; |
|
36 |
||
37 |
val uses = Scan.optional (Parse.$$$ usesN |-- Parse.!!! (Scan.repeat1 file)) []; |
|
22106 | 38 |
|
39 |
val args = |
|
36950 | 40 |
theory_name -- (Parse.$$$ importsN |-- |
41 |
Parse.!!! (Scan.repeat1 theory_name -- uses --| Parse.$$$ beginN)) |
|
42 |
>> Parse.triple2; |
|
22106 | 43 |
|
44 |
||
45 |
(* read header *) |
|
46 |
||
47 |
val header = |
|
36950 | 48 |
(Parse.$$$ headerN -- Parse.tags) |-- |
49 |
(Parse.!!! (Parse.doc_source -- Scan.repeat Parse.semicolon -- |
|
50 |
(Parse.$$$ theoryN -- Parse.tags) |-- args)) || |
|
51 |
(Parse.$$$ theoryN -- Parse.tags) |-- Parse.!!! args; |
|
22106 | 52 |
|
23863 | 53 |
fun read pos src = |
22106 | 54 |
let val res = |
55 |
src |
|
27835
ff8b8513965a
Symbol.source/OuterLex.source: more explicit do_recover argument;
wenzelm
parents:
24739
diff
changeset
|
56 |
|> Symbol.source {do_recover = false} |
36959
f5417836dbea
renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents:
36950
diff
changeset
|
57 |
|> Token.source {do_recover = NONE} (fn () => (header_lexicon, Scan.empty_lexicon)) pos |
f5417836dbea
renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents:
36950
diff
changeset
|
58 |
|> Token.source_proper |
f5417836dbea
renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents:
36950
diff
changeset
|
59 |
|> Source.source Token.stopper (Scan.single (Scan.error (Parse.!!! header))) NONE |
22106 | 60 |
|> Source.get_single; |
61 |
in |
|
62 |
(case res of SOME (x, _) => x |
|
63 |
| NONE => error ("Unexpected end of input" ^ Position.str_of pos)) |
|
64 |
end; |
|
65 |
||
66 |
end; |