author | wenzelm |
Fri, 15 Aug 2008 15:51:06 +0200 | |
changeset 27890 | 62ac62e30ab1 |
parent 27872 | 631371a02b8c |
child 29606 | fedb8be05f24 |
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 |
||
27890
62ac62e30ab1
args: explicit groups for file_name, theory_name;
wenzelm
parents:
27872
diff
changeset
|
36 |
val file_name = P.group "file name" P.name; |
62ac62e30ab1
args: explicit groups for file_name, theory_name;
wenzelm
parents:
27872
diff
changeset
|
37 |
val theory_name = P.group "theory name" P.name; |
62ac62e30ab1
args: explicit groups for file_name, theory_name;
wenzelm
parents:
27872
diff
changeset
|
38 |
|
62ac62e30ab1
args: explicit groups for file_name, theory_name;
wenzelm
parents:
27872
diff
changeset
|
39 |
val file = (P.$$$ "(" |-- P.!!! (file_name --| P.$$$ ")")) >> rpair false || file_name >> rpair true; |
22106 | 40 |
val uses = Scan.optional (P.$$$ usesN |-- P.!!! (Scan.repeat1 file)) []; |
41 |
||
42 |
val args = |
|
27890
62ac62e30ab1
args: explicit groups for file_name, theory_name;
wenzelm
parents:
27872
diff
changeset
|
43 |
theory_name -- (P.$$$ importsN |-- P.!!! (Scan.repeat1 theory_name -- uses --| P.$$$ beginN)) |
22106 | 44 |
>> P.triple2; |
45 |
||
46 |
||
47 |
(* read header *) |
|
48 |
||
49 |
val header = |
|
27872
631371a02b8c
P.doc_source and P.ml_sorce for proper SymbolPos.text;
wenzelm
parents:
27835
diff
changeset
|
50 |
(P.$$$ headerN -- P.tags) |-- (P.!!! (P.doc_source -- Scan.repeat P.semicolon -- |
22106 | 51 |
(P.$$$ theoryN -- P.tags) |-- args)) || |
52 |
(P.$$$ theoryN -- P.tags) |-- P.!!! args; |
|
53 |
||
23863 | 54 |
fun read pos src = |
22106 | 55 |
let val res = |
56 |
src |
|
27835
ff8b8513965a
Symbol.source/OuterLex.source: more explicit do_recover argument;
wenzelm
parents:
24739
diff
changeset
|
57 |
|> Symbol.source {do_recover = false} |
ff8b8513965a
Symbol.source/OuterLex.source: more explicit do_recover argument;
wenzelm
parents:
24739
diff
changeset
|
58 |
|> T.source {do_recover = NONE} (fn () => (header_lexicon, Scan.empty_lexicon)) pos |
22106 | 59 |
|> T.source_proper |
24739 | 60 |
|> Source.source T.stopper (Scan.single (Scan.error (P.!!! header))) NONE |
22106 | 61 |
|> Source.get_single; |
62 |
in |
|
63 |
(case res of SOME (x, _) => x |
|
64 |
| NONE => error ("Unexpected end of input" ^ Position.str_of pos)) |
|
65 |
end; |
|
66 |
||
67 |
end; |