author | haftmann |
Mon, 19 Sep 2005 16:38:35 +0200 | |
changeset 17485 | c39871c52977 |
parent 17075 | 5e9c1b81b690 |
child 17933 | b8f2dd8858f6 |
permissions | -rw-r--r-- |
9139 | 1 |
(* Title: Pure/Isar/thy_header.ML |
2 |
ID: $Id$ |
|
3 |
Author: Markus Wenzel, TU Muenchen |
|
4 |
||
5 |
Theory headers (old and new-style). |
|
6 |
*) |
|
7 |
||
8 |
signature THY_HEADER = |
|
9 |
sig |
|
10 |
val is_old: (string, 'a) Source.source * Position.T -> bool |
|
11 |
val args: OuterLex.token list -> |
|
12 |
(string * string list * (string * bool) list) * OuterLex.token list |
|
16265
ee2497cde564
new Isar header: reject ':', accept both 'files' and 'uses';
wenzelm
parents:
15531
diff
changeset
|
13 |
val scan: (string, 'a) Source.source * Position.T -> |
ee2497cde564
new Isar header: reject ':', accept both 'files' and 'uses';
wenzelm
parents:
15531
diff
changeset
|
14 |
string * string list * (string * bool) list |
9139 | 15 |
end; |
16 |
||
17 |
structure ThyHeader: THY_HEADER = |
|
18 |
struct |
|
19 |
||
20 |
structure T = OuterLex; |
|
21 |
structure P = OuterParse; |
|
22 |
||
23 |
||
24 |
(* scan header *) |
|
25 |
||
26 |
fun scan_header get_lex scan (src, pos) = |
|
12840 | 27 |
let val res = |
28 |
src |
|
29 |
|> Symbol.source false |
|
30 |
|> T.source false (fn () => (get_lex (), Scan.empty_lexicon)) pos |
|
31 |
|> T.source_proper |
|
15531 | 32 |
|> Source.source T.stopper (Scan.single scan) NONE |
12840 | 33 |
|> Source.get_single; |
34 |
in |
|
15531 | 35 |
(case res of SOME (x, _) => x |
36 |
| NONE => error ("Unexpected end of input" ^ Position.str_of pos)) |
|
12840 | 37 |
end; |
9139 | 38 |
|
39 |
||
40 |
(* keywords *) |
|
41 |
||
42 |
val headerN = "header"; |
|
43 |
val theoryN = "theory"; |
|
15141 | 44 |
val importsN = "imports"; |
16265
ee2497cde564
new Isar header: reject ':', accept both 'files' and 'uses';
wenzelm
parents:
15531
diff
changeset
|
45 |
val filesN = "files"; |
ee2497cde564
new Isar header: reject ':', accept both 'files' and 'uses';
wenzelm
parents:
15531
diff
changeset
|
46 |
val usesN = "uses"; |
ee2497cde564
new Isar header: reject ':', accept both 'files' and 'uses';
wenzelm
parents:
15531
diff
changeset
|
47 |
val beginN = "begin"; |
9139 | 48 |
|
49 |
||
50 |
(* detect new/old headers *) |
|
51 |
||
52 |
val check_header_lexicon = T.make_lexicon [headerN, theoryN]; |
|
16265
ee2497cde564
new Isar header: reject ':', accept both 'files' and 'uses';
wenzelm
parents:
15531
diff
changeset
|
53 |
val check_header = Scan.option (P.$$$ headerN || P.$$$ theoryN); |
9139 | 54 |
|
55 |
fun is_old src_pos = |
|
16265
ee2497cde564
new Isar header: reject ':', accept both 'files' and 'uses';
wenzelm
parents:
15531
diff
changeset
|
56 |
is_none (scan_header (K check_header_lexicon) check_header src_pos); |
9139 | 57 |
|
58 |
||
59 |
(* scan old/new headers *) |
|
60 |
||
15132 | 61 |
val header_lexicon = T.make_lexicon |
17075 | 62 |
["%", "(", ")", "+", ":", ";", "=", beginN, filesN, headerN, importsN, theoryN, usesN]; |
9139 | 63 |
|
16265
ee2497cde564
new Isar header: reject ':', accept both 'files' and 'uses';
wenzelm
parents:
15531
diff
changeset
|
64 |
val file = |
9139 | 65 |
(P.$$$ "(" |-- P.!!! (P.name --| P.$$$ ")")) >> rpair false || P.name >> rpair true; |
16265
ee2497cde564
new Isar header: reject ':', accept both 'files' and 'uses';
wenzelm
parents:
15531
diff
changeset
|
66 |
fun files keyword = Scan.optional (keyword |-- P.!!! (Scan.repeat1 file)) []; |
9139 | 67 |
|
68 |
val args = |
|
16265
ee2497cde564
new Isar header: reject ':', accept both 'files' and 'uses';
wenzelm
parents:
15531
diff
changeset
|
69 |
P.name -- |
ee2497cde564
new Isar header: reject ':', accept both 'files' and 'uses';
wenzelm
parents:
15531
diff
changeset
|
70 |
(P.$$$ "=" |-- P.!!! (P.enum1 "+" P.name -- files (P.$$$ filesN) --| P.$$$ ":") || |
17075 | 71 |
P.$$$ importsN |-- P.!!! (Scan.repeat1 P.name -- files (P.$$$ usesN) --| P.$$$ beginN)) |
16265
ee2497cde564
new Isar header: reject ':', accept both 'files' and 'uses';
wenzelm
parents:
15531
diff
changeset
|
72 |
>> P.triple2; |
9139 | 73 |
|
74 |
||
75 |
val new_header = |
|
17075 | 76 |
(P.$$$ headerN -- P.tags) |-- (P.!!! (P.text -- Scan.repeat P.semicolon -- |
77 |
(P.$$$ theoryN -- P.tags) |-- args)) || |
|
78 |
(P.$$$ theoryN -- P.tags) |-- P.!!! args; |
|
9139 | 79 |
|
80 |
val old_header = |
|
81 |
P.!!! (P.group "theory header" |
|
82 |
(P.name -- (P.$$$ "=" |-- P.name -- Scan.repeat (P.$$$ "+" |-- P.name)))) |
|
83 |
>> (fn (A, (B, Bs)) => (A, B :: Bs, []: (string * bool) list)); |
|
84 |
||
85 |
fun scan src_pos = |
|
86 |
(*sadly, old-style headers depend on the current (dynamic!) lexicon*) |
|
87 |
if is_old src_pos then |
|
88 |
scan_header ThySyn.get_lexicon (Scan.error old_header) src_pos |
|
89 |
else scan_header (K header_lexicon) (Scan.error new_header) src_pos; |
|
90 |
||
91 |
||
92 |
end; |