author | wenzelm |
Sun, 10 Dec 2006 15:30:45 +0100 | |
changeset 21746 | 9d0652354513 |
parent 17978 | b48885914c1d |
permissions | -rw-r--r-- |
9139 | 1 |
(* Title: Pure/Isar/thy_header.ML |
2 |
ID: $Id$ |
|
3 |
Author: Markus Wenzel, TU Muenchen |
|
4 |
||
17978 | 5 |
Theory headers -- processed separately with minimal outer syntax. |
9139 | 6 |
*) |
7 |
||
8 |
signature THY_HEADER = |
|
9 |
sig |
|
10 |
val args: OuterLex.token list -> |
|
11 |
(string * string list * (string * bool) list) * OuterLex.token list |
|
17933
b8f2dd8858f6
removed obsolete non-Isar theory format and old Isar theory headers;
wenzelm
parents:
17075
diff
changeset
|
12 |
val read: (string, 'a) Source.source * Position.T -> |
16265
ee2497cde564
new Isar header: reject ':', accept both 'files' and 'uses';
wenzelm
parents:
15531
diff
changeset
|
13 |
string * string list * (string * bool) list |
9139 | 14 |
end; |
15 |
||
16 |
structure ThyHeader: THY_HEADER = |
|
17 |
struct |
|
18 |
||
19 |
structure T = OuterLex; |
|
20 |
structure P = OuterParse; |
|
21 |
||
22 |
||
17933
b8f2dd8858f6
removed obsolete non-Isar theory format and old Isar theory headers;
wenzelm
parents:
17075
diff
changeset
|
23 |
(* keywords *) |
b8f2dd8858f6
removed obsolete non-Isar theory format and old Isar theory headers;
wenzelm
parents:
17075
diff
changeset
|
24 |
|
b8f2dd8858f6
removed obsolete non-Isar theory format and old Isar theory headers;
wenzelm
parents:
17075
diff
changeset
|
25 |
val headerN = "header"; |
b8f2dd8858f6
removed obsolete non-Isar theory format and old Isar theory headers;
wenzelm
parents:
17075
diff
changeset
|
26 |
val theoryN = "theory"; |
b8f2dd8858f6
removed obsolete non-Isar theory format and old Isar theory headers;
wenzelm
parents:
17075
diff
changeset
|
27 |
val importsN = "imports"; |
b8f2dd8858f6
removed obsolete non-Isar theory format and old Isar theory headers;
wenzelm
parents:
17075
diff
changeset
|
28 |
val usesN = "uses"; |
b8f2dd8858f6
removed obsolete non-Isar theory format and old Isar theory headers;
wenzelm
parents:
17075
diff
changeset
|
29 |
val beginN = "begin"; |
b8f2dd8858f6
removed obsolete non-Isar theory format and old Isar theory headers;
wenzelm
parents:
17075
diff
changeset
|
30 |
|
b8f2dd8858f6
removed obsolete non-Isar theory format and old Isar theory headers;
wenzelm
parents:
17075
diff
changeset
|
31 |
val header_lexicon = T.make_lexicon |
b8f2dd8858f6
removed obsolete non-Isar theory format and old Isar theory headers;
wenzelm
parents:
17075
diff
changeset
|
32 |
["%", "(", ")", ";", beginN, headerN, importsN, theoryN, usesN]; |
b8f2dd8858f6
removed obsolete non-Isar theory format and old Isar theory headers;
wenzelm
parents:
17075
diff
changeset
|
33 |
|
b8f2dd8858f6
removed obsolete non-Isar theory format and old Isar theory headers;
wenzelm
parents:
17075
diff
changeset
|
34 |
|
b8f2dd8858f6
removed obsolete non-Isar theory format and old Isar theory headers;
wenzelm
parents:
17075
diff
changeset
|
35 |
(* header args *) |
9139 | 36 |
|
17933
b8f2dd8858f6
removed obsolete non-Isar theory format and old Isar theory headers;
wenzelm
parents:
17075
diff
changeset
|
37 |
val file = (P.$$$ "(" |-- P.!!! (P.name --| P.$$$ ")")) >> rpair false || P.name >> rpair true; |
b8f2dd8858f6
removed obsolete non-Isar theory format and old Isar theory headers;
wenzelm
parents:
17075
diff
changeset
|
38 |
val uses = Scan.optional (P.$$$ usesN |-- P.!!! (Scan.repeat1 file)) []; |
b8f2dd8858f6
removed obsolete non-Isar theory format and old Isar theory headers;
wenzelm
parents:
17075
diff
changeset
|
39 |
|
b8f2dd8858f6
removed obsolete non-Isar theory format and old Isar theory headers;
wenzelm
parents:
17075
diff
changeset
|
40 |
val args = |
b8f2dd8858f6
removed obsolete non-Isar theory format and old Isar theory headers;
wenzelm
parents:
17075
diff
changeset
|
41 |
P.name -- (P.$$$ importsN |-- P.!!! (Scan.repeat1 P.name -- uses --| P.$$$ beginN)) |
b8f2dd8858f6
removed obsolete non-Isar theory format and old Isar theory headers;
wenzelm
parents:
17075
diff
changeset
|
42 |
>> P.triple2; |
b8f2dd8858f6
removed obsolete non-Isar theory format and old Isar theory headers;
wenzelm
parents:
17075
diff
changeset
|
43 |
|
b8f2dd8858f6
removed obsolete non-Isar theory format and old Isar theory headers;
wenzelm
parents:
17075
diff
changeset
|
44 |
|
b8f2dd8858f6
removed obsolete non-Isar theory format and old Isar theory headers;
wenzelm
parents:
17075
diff
changeset
|
45 |
(* read header *) |
b8f2dd8858f6
removed obsolete non-Isar theory format and old Isar theory headers;
wenzelm
parents:
17075
diff
changeset
|
46 |
|
b8f2dd8858f6
removed obsolete non-Isar theory format and old Isar theory headers;
wenzelm
parents:
17075
diff
changeset
|
47 |
val header = |
b8f2dd8858f6
removed obsolete non-Isar theory format and old Isar theory headers;
wenzelm
parents:
17075
diff
changeset
|
48 |
(P.$$$ headerN -- P.tags) |-- (P.!!! (P.text -- Scan.repeat P.semicolon -- |
b8f2dd8858f6
removed obsolete non-Isar theory format and old Isar theory headers;
wenzelm
parents:
17075
diff
changeset
|
49 |
(P.$$$ theoryN -- P.tags) |-- args)) || |
b8f2dd8858f6
removed obsolete non-Isar theory format and old Isar theory headers;
wenzelm
parents:
17075
diff
changeset
|
50 |
(P.$$$ theoryN -- P.tags) |-- P.!!! args; |
b8f2dd8858f6
removed obsolete non-Isar theory format and old Isar theory headers;
wenzelm
parents:
17075
diff
changeset
|
51 |
|
b8f2dd8858f6
removed obsolete non-Isar theory format and old Isar theory headers;
wenzelm
parents:
17075
diff
changeset
|
52 |
fun read (src, pos) = |
12840 | 53 |
let val res = |
54 |
src |
|
55 |
|> Symbol.source false |
|
17933
b8f2dd8858f6
removed obsolete non-Isar theory format and old Isar theory headers;
wenzelm
parents:
17075
diff
changeset
|
56 |
|> T.source false (fn () => (header_lexicon, Scan.empty_lexicon)) pos |
12840 | 57 |
|> T.source_proper |
17933
b8f2dd8858f6
removed obsolete non-Isar theory format and old Isar theory headers;
wenzelm
parents:
17075
diff
changeset
|
58 |
|> Source.source T.stopper (Scan.single (Scan.error header)) NONE |
12840 | 59 |
|> Source.get_single; |
60 |
in |
|
15531 | 61 |
(case res of SOME (x, _) => x |
62 |
| NONE => error ("Unexpected end of input" ^ Position.str_of pos)) |
|
12840 | 63 |
end; |
9139 | 64 |
|
65 |
end; |