|
1 (* Title: Pure/Isar/thy_header.ML |
|
2 ID: $Id$ |
|
3 Author: Markus Wenzel, TU Muenchen |
|
4 License: GPL (GNU GENERAL PUBLIC LICENSE) |
|
5 |
|
6 Theory headers (old and new-style). |
|
7 *) |
|
8 |
|
9 signature THY_HEADER = |
|
10 sig |
|
11 val is_old: (string, 'a) Source.source * Position.T -> bool |
|
12 val args: OuterLex.token list -> |
|
13 (string * string list * (string * bool) list) * OuterLex.token list |
|
14 val scan: (string, 'a) Source.source * Position.T -> string * string list * (string * bool) list |
|
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) = |
|
27 src |
|
28 |> Symbol.source false |
|
29 |> T.source false (fn () => (get_lex (), Scan.empty_lexicon)) pos |
|
30 |> T.source_proper |
|
31 |> Source.source T.stopper (Scan.single scan) None |
|
32 |> (fst o the o Source.get_single); |
|
33 |
|
34 |
|
35 (* keywords *) |
|
36 |
|
37 val headerN = "header"; |
|
38 val theoryN = "theory"; |
|
39 |
|
40 val theory_keyword = P.$$$ theoryN; |
|
41 val header_keyword = P.$$$ headerN; |
|
42 |
|
43 |
|
44 (* detect new/old headers *) |
|
45 |
|
46 val check_header_lexicon = T.make_lexicon [headerN, theoryN]; |
|
47 val check_header = Scan.option (header_keyword || theory_keyword); |
|
48 |
|
49 fun is_old src_pos = |
|
50 Library.is_none (scan_header (K check_header_lexicon) check_header src_pos); |
|
51 |
|
52 |
|
53 (* scan old/new headers *) |
|
54 |
|
55 val header_lexicon = |
|
56 T.make_lexicon ["(", ")", "+", ":", ";", "=", "files", headerN, theoryN]; |
|
57 |
|
58 val file_name = |
|
59 (P.$$$ "(" |-- P.!!! (P.name --| P.$$$ ")")) >> rpair false || P.name >> rpair true; |
|
60 |
|
61 |
|
62 val args = |
|
63 (P.name -- (P.$$$ "=" |-- P.enum1 "+" P.name) -- |
|
64 Scan.optional (P.$$$ "files" |-- P.!!! (Scan.repeat1 file_name)) [] --| P.$$$ ":") |
|
65 >> (fn ((A, Bs), files) => (A, Bs, files)); |
|
66 |
|
67 |
|
68 val new_header = |
|
69 header_keyword |-- (P.!!! (P.text -- Scan.repeat P.semicolon -- theory_keyword |-- args)) || |
|
70 theory_keyword |-- P.!!! args; |
|
71 |
|
72 val old_header = |
|
73 P.!!! (P.group "theory header" |
|
74 (P.name -- (P.$$$ "=" |-- P.name -- Scan.repeat (P.$$$ "+" |-- P.name)))) |
|
75 >> (fn (A, (B, Bs)) => (A, B :: Bs, []: (string * bool) list)); |
|
76 |
|
77 fun scan src_pos = |
|
78 (*sadly, old-style headers depend on the current (dynamic!) lexicon*) |
|
79 if is_old src_pos then |
|
80 scan_header ThySyn.get_lexicon (Scan.error old_header) src_pos |
|
81 else scan_header (K header_lexicon) (Scan.error new_header) src_pos; |
|
82 |
|
83 |
|
84 end; |