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