author | wenzelm |
Sat, 21 Jul 2012 22:13:50 +0200 | |
changeset 48421 | c4d337782de4 |
parent 46961 | 5c6955f487e5 |
child 48638 | 22d65e375c01 |
permissions | -rw-r--r-- |
22106 | 1 |
(* Title: Pure/Thy/thy_header.ML |
46939 | 2 |
Author: Makarius |
22106 | 3 |
|
46939 | 4 |
Static theory header information. |
22106 | 5 |
*) |
6 |
||
7 |
signature THY_HEADER = |
|
8 |
sig |
|
46938
cda018294515
some support for outer syntax keyword declarations within theory header;
wenzelm
parents:
46737
diff
changeset
|
9 |
type header = |
cda018294515
some support for outer syntax keyword declarations within theory header;
wenzelm
parents:
46737
diff
changeset
|
10 |
{name: string, imports: string list, |
46961
5c6955f487e5
outer syntax command definitions based on formal command_spec derived from theory header declarations;
wenzelm
parents:
46958
diff
changeset
|
11 |
keywords: (string * Keyword.spec option) list, |
46938
cda018294515
some support for outer syntax keyword declarations within theory header;
wenzelm
parents:
46737
diff
changeset
|
12 |
uses: (Path.T * bool) list} |
46961
5c6955f487e5
outer syntax command definitions based on formal command_spec derived from theory header declarations;
wenzelm
parents:
46958
diff
changeset
|
13 |
val make: string -> string list -> (string * Keyword.spec option) list -> |
46938
cda018294515
some support for outer syntax keyword declarations within theory header;
wenzelm
parents:
46737
diff
changeset
|
14 |
(Path.T * bool) list -> header |
46958
0ec8f04e753a
define keywords early when processing the theory header, before running the body commands;
wenzelm
parents:
46950
diff
changeset
|
15 |
val define_keywords: header -> unit |
46961
5c6955f487e5
outer syntax command definitions based on formal command_spec derived from theory header declarations;
wenzelm
parents:
46958
diff
changeset
|
16 |
val declare_keyword: string * Keyword.spec option -> theory -> theory |
5c6955f487e5
outer syntax command definitions based on formal command_spec derived from theory header declarations;
wenzelm
parents:
46958
diff
changeset
|
17 |
val the_keyword: theory -> string -> Keyword.spec option |
46938
cda018294515
some support for outer syntax keyword declarations within theory header;
wenzelm
parents:
46737
diff
changeset
|
18 |
val args: header parser |
cda018294515
some support for outer syntax keyword declarations within theory header;
wenzelm
parents:
46737
diff
changeset
|
19 |
val read: Position.T -> string -> header |
22106 | 20 |
end; |
21 |
||
32466 | 22 |
structure Thy_Header: THY_HEADER = |
22106 | 23 |
struct |
24 |
||
46938
cda018294515
some support for outer syntax keyword declarations within theory header;
wenzelm
parents:
46737
diff
changeset
|
25 |
type header = |
cda018294515
some support for outer syntax keyword declarations within theory header;
wenzelm
parents:
46737
diff
changeset
|
26 |
{name: string, imports: string list, |
46961
5c6955f487e5
outer syntax command definitions based on formal command_spec derived from theory header declarations;
wenzelm
parents:
46958
diff
changeset
|
27 |
keywords: (string * Keyword.spec option) list, |
46938
cda018294515
some support for outer syntax keyword declarations within theory header;
wenzelm
parents:
46737
diff
changeset
|
28 |
uses: (Path.T * bool) list}; |
cda018294515
some support for outer syntax keyword declarations within theory header;
wenzelm
parents:
46737
diff
changeset
|
29 |
|
cda018294515
some support for outer syntax keyword declarations within theory header;
wenzelm
parents:
46737
diff
changeset
|
30 |
fun make name imports keywords uses : header = |
cda018294515
some support for outer syntax keyword declarations within theory header;
wenzelm
parents:
46737
diff
changeset
|
31 |
{name = name, imports = imports, keywords = keywords, uses = uses}; |
cda018294515
some support for outer syntax keyword declarations within theory header;
wenzelm
parents:
46737
diff
changeset
|
32 |
|
cda018294515
some support for outer syntax keyword declarations within theory header;
wenzelm
parents:
46737
diff
changeset
|
33 |
|
cda018294515
some support for outer syntax keyword declarations within theory header;
wenzelm
parents:
46737
diff
changeset
|
34 |
|
cda018294515
some support for outer syntax keyword declarations within theory header;
wenzelm
parents:
46737
diff
changeset
|
35 |
(** keyword declarations **) |
cda018294515
some support for outer syntax keyword declarations within theory header;
wenzelm
parents:
46737
diff
changeset
|
36 |
|
46958
0ec8f04e753a
define keywords early when processing the theory header, before running the body commands;
wenzelm
parents:
46950
diff
changeset
|
37 |
fun define_keywords ({keywords, ...}: header) = |
46961
5c6955f487e5
outer syntax command definitions based on formal command_spec derived from theory header declarations;
wenzelm
parents:
46958
diff
changeset
|
38 |
List.app (Keyword.define o apsnd (Option.map Keyword.spec)) keywords; |
46958
0ec8f04e753a
define keywords early when processing the theory header, before running the body commands;
wenzelm
parents:
46950
diff
changeset
|
39 |
|
46938
cda018294515
some support for outer syntax keyword declarations within theory header;
wenzelm
parents:
46737
diff
changeset
|
40 |
fun err_dup name = error ("Inconsistent declaration of outer syntax keyword " ^ quote name); |
cda018294515
some support for outer syntax keyword declarations within theory header;
wenzelm
parents:
46737
diff
changeset
|
41 |
|
cda018294515
some support for outer syntax keyword declarations within theory header;
wenzelm
parents:
46737
diff
changeset
|
42 |
structure Data = Theory_Data |
cda018294515
some support for outer syntax keyword declarations within theory header;
wenzelm
parents:
46737
diff
changeset
|
43 |
( |
46961
5c6955f487e5
outer syntax command definitions based on formal command_spec derived from theory header declarations;
wenzelm
parents:
46958
diff
changeset
|
44 |
type T = Keyword.spec option Symtab.table; |
46938
cda018294515
some support for outer syntax keyword declarations within theory header;
wenzelm
parents:
46737
diff
changeset
|
45 |
val empty = Symtab.empty; |
cda018294515
some support for outer syntax keyword declarations within theory header;
wenzelm
parents:
46737
diff
changeset
|
46 |
val extend = I; |
cda018294515
some support for outer syntax keyword declarations within theory header;
wenzelm
parents:
46737
diff
changeset
|
47 |
fun merge data : T = Symtab.merge (op =) data handle Symtab.DUP name => err_dup name; |
cda018294515
some support for outer syntax keyword declarations within theory header;
wenzelm
parents:
46737
diff
changeset
|
48 |
); |
cda018294515
some support for outer syntax keyword declarations within theory header;
wenzelm
parents:
46737
diff
changeset
|
49 |
|
46961
5c6955f487e5
outer syntax command definitions based on formal command_spec derived from theory header declarations;
wenzelm
parents:
46958
diff
changeset
|
50 |
fun declare_keyword (name, spec) = |
5c6955f487e5
outer syntax command definitions based on formal command_spec derived from theory header declarations;
wenzelm
parents:
46958
diff
changeset
|
51 |
Data.map (fn data => |
5c6955f487e5
outer syntax command definitions based on formal command_spec derived from theory header declarations;
wenzelm
parents:
46958
diff
changeset
|
52 |
(Option.map Keyword.spec spec; |
5c6955f487e5
outer syntax command definitions based on formal command_spec derived from theory header declarations;
wenzelm
parents:
46958
diff
changeset
|
53 |
Symtab.update_new (name, spec) data handle Symtab.DUP dup => err_dup dup)); |
46938
cda018294515
some support for outer syntax keyword declarations within theory header;
wenzelm
parents:
46737
diff
changeset
|
54 |
|
cda018294515
some support for outer syntax keyword declarations within theory header;
wenzelm
parents:
46737
diff
changeset
|
55 |
fun the_keyword thy name = |
cda018294515
some support for outer syntax keyword declarations within theory header;
wenzelm
parents:
46737
diff
changeset
|
56 |
(case Symtab.lookup (Data.get thy) name of |
46961
5c6955f487e5
outer syntax command definitions based on formal command_spec derived from theory header declarations;
wenzelm
parents:
46958
diff
changeset
|
57 |
SOME spec => spec |
5c6955f487e5
outer syntax command definitions based on formal command_spec derived from theory header declarations;
wenzelm
parents:
46958
diff
changeset
|
58 |
| NONE => error ("Undeclared outer syntax keyword " ^ quote name)); |
46938
cda018294515
some support for outer syntax keyword declarations within theory header;
wenzelm
parents:
46737
diff
changeset
|
59 |
|
cda018294515
some support for outer syntax keyword declarations within theory header;
wenzelm
parents:
46737
diff
changeset
|
60 |
|
cda018294515
some support for outer syntax keyword declarations within theory header;
wenzelm
parents:
46737
diff
changeset
|
61 |
|
cda018294515
some support for outer syntax keyword declarations within theory header;
wenzelm
parents:
46737
diff
changeset
|
62 |
(** concrete syntax **) |
cda018294515
some support for outer syntax keyword declarations within theory header;
wenzelm
parents:
46737
diff
changeset
|
63 |
|
cda018294515
some support for outer syntax keyword declarations within theory header;
wenzelm
parents:
46737
diff
changeset
|
64 |
(* header keywords *) |
22106 | 65 |
|
66 |
val headerN = "header"; |
|
67 |
val theoryN = "theory"; |
|
68 |
val importsN = "imports"; |
|
46938
cda018294515
some support for outer syntax keyword declarations within theory header;
wenzelm
parents:
46737
diff
changeset
|
69 |
val keywordsN = "keywords"; |
22106 | 70 |
val usesN = "uses"; |
71 |
val beginN = "begin"; |
|
72 |
||
46938
cda018294515
some support for outer syntax keyword declarations within theory header;
wenzelm
parents:
46737
diff
changeset
|
73 |
val header_lexicon = |
cda018294515
some support for outer syntax keyword declarations within theory header;
wenzelm
parents:
46737
diff
changeset
|
74 |
Scan.make_lexicon |
cda018294515
some support for outer syntax keyword declarations within theory header;
wenzelm
parents:
46737
diff
changeset
|
75 |
(map Symbol.explode |
cda018294515
some support for outer syntax keyword declarations within theory header;
wenzelm
parents:
46737
diff
changeset
|
76 |
["%", "(", ")", "::", ";", "and", beginN, headerN, importsN, keywordsN, theoryN, usesN]); |
22106 | 77 |
|
78 |
||
79 |
(* header args *) |
|
80 |
||
46938
cda018294515
some support for outer syntax keyword declarations within theory header;
wenzelm
parents:
46737
diff
changeset
|
81 |
local |
cda018294515
some support for outer syntax keyword declarations within theory header;
wenzelm
parents:
46737
diff
changeset
|
82 |
|
cda018294515
some support for outer syntax keyword declarations within theory header;
wenzelm
parents:
46737
diff
changeset
|
83 |
val file_name = Parse.group (fn () => "file name") Parse.path; |
44357 | 84 |
val theory_name = Parse.group (fn () => "theory name") Parse.name; |
27890
62ac62e30ab1
args: explicit groups for file_name, theory_name;
wenzelm
parents:
27872
diff
changeset
|
85 |
|
46938
cda018294515
some support for outer syntax keyword declarations within theory header;
wenzelm
parents:
46737
diff
changeset
|
86 |
val keyword_kind = Parse.group (fn () => "outer syntax keyword kind") (Parse.name -- Parse.tags); |
46939 | 87 |
val keyword_decl = |
46943 | 88 |
Scan.repeat1 Parse.string -- Scan.option (Parse.$$$ "::" |-- Parse.!!! keyword_kind) >> |
46939 | 89 |
(fn (names, kind) => map (rpair kind) names); |
90 |
val keyword_decls = Parse.and_list1 keyword_decl >> flat; |
|
46938
cda018294515
some support for outer syntax keyword declarations within theory header;
wenzelm
parents:
46737
diff
changeset
|
91 |
|
36950 | 92 |
val file = |
93 |
Parse.$$$ "(" |-- Parse.!!! (file_name --| Parse.$$$ ")") >> rpair false || |
|
94 |
file_name >> rpair true; |
|
95 |
||
46938
cda018294515
some support for outer syntax keyword declarations within theory header;
wenzelm
parents:
46737
diff
changeset
|
96 |
in |
22106 | 97 |
|
98 |
val args = |
|
46938
cda018294515
some support for outer syntax keyword declarations within theory header;
wenzelm
parents:
46737
diff
changeset
|
99 |
theory_name -- |
cda018294515
some support for outer syntax keyword declarations within theory header;
wenzelm
parents:
46737
diff
changeset
|
100 |
(Parse.$$$ importsN |-- Parse.!!! (Scan.repeat1 theory_name)) -- |
46939 | 101 |
Scan.optional (Parse.$$$ keywordsN |-- Parse.!!! keyword_decls) [] -- |
46938
cda018294515
some support for outer syntax keyword declarations within theory header;
wenzelm
parents:
46737
diff
changeset
|
102 |
Scan.optional (Parse.$$$ usesN |-- Parse.!!! (Scan.repeat1 file)) [] --| |
cda018294515
some support for outer syntax keyword declarations within theory header;
wenzelm
parents:
46737
diff
changeset
|
103 |
Parse.$$$ beginN >> |
cda018294515
some support for outer syntax keyword declarations within theory header;
wenzelm
parents:
46737
diff
changeset
|
104 |
(fn (((name, imports), keywords), uses) => make name imports keywords uses); |
cda018294515
some support for outer syntax keyword declarations within theory header;
wenzelm
parents:
46737
diff
changeset
|
105 |
|
cda018294515
some support for outer syntax keyword declarations within theory header;
wenzelm
parents:
46737
diff
changeset
|
106 |
end; |
22106 | 107 |
|
108 |
||
109 |
(* read header *) |
|
110 |
||
111 |
val header = |
|
36950 | 112 |
(Parse.$$$ headerN -- Parse.tags) |-- |
113 |
(Parse.!!! (Parse.doc_source -- Scan.repeat Parse.semicolon -- |
|
114 |
(Parse.$$$ theoryN -- Parse.tags) |-- args)) || |
|
115 |
(Parse.$$$ theoryN -- Parse.tags) |-- Parse.!!! args; |
|
22106 | 116 |
|
37978
548f3f165d05
simplified Thy_Header.read -- include Source.of_string_limited here;
wenzelm
parents:
37950
diff
changeset
|
117 |
fun read pos str = |
22106 | 118 |
let val res = |
37978
548f3f165d05
simplified Thy_Header.read -- include Source.of_string_limited here;
wenzelm
parents:
37950
diff
changeset
|
119 |
str |
548f3f165d05
simplified Thy_Header.read -- include Source.of_string_limited here;
wenzelm
parents:
37950
diff
changeset
|
120 |
|> Source.of_string_limited 8000 |
40523
1050315f6ee2
simplified/robustified treatment of malformed symbols, which are now fully internalized (total Symbol.explode etc.);
wenzelm
parents:
38149
diff
changeset
|
121 |
|> Symbol.source |
36959
f5417836dbea
renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents:
36950
diff
changeset
|
122 |
|> Token.source {do_recover = NONE} (fn () => (header_lexicon, Scan.empty_lexicon)) pos |
f5417836dbea
renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents:
36950
diff
changeset
|
123 |
|> Token.source_proper |
f5417836dbea
renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents:
36950
diff
changeset
|
124 |
|> Source.source Token.stopper (Scan.single (Scan.error (Parse.!!! header))) NONE |
22106 | 125 |
|> Source.get_single; |
126 |
in |
|
42003
6e45dc518ebb
replaced File.check by specific File.check_file, File.check_dir;
wenzelm
parents:
41944
diff
changeset
|
127 |
(case res of |
46938
cda018294515
some support for outer syntax keyword declarations within theory header;
wenzelm
parents:
46737
diff
changeset
|
128 |
SOME (h, _) => h |
22106 | 129 |
| NONE => error ("Unexpected end of input" ^ Position.str_of pos)) |
130 |
end; |
|
131 |
||
132 |
end; |