author | wenzelm |
Wed, 22 Aug 2012 12:47:49 +0200 | |
changeset 48881 | 46e053eda5dd |
parent 48874 | ff9cd47be39b |
child 48927 | ef462b5558eb |
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 |
|
48874
ff9cd47be39b
refined Thy_Load.check_thy: find more uses in body text, based on keywords;
wenzelm
parents:
48864
diff
changeset
|
9 |
type keywords = (string * Keyword.spec option) list |
46938
cda018294515
some support for outer syntax keyword declarations within theory header;
wenzelm
parents:
46737
diff
changeset
|
10 |
type header = |
48707
ba531af91148
simplified Document.Node.Header -- internalized errors;
wenzelm
parents:
48638
diff
changeset
|
11 |
{name: string, |
ba531af91148
simplified Document.Node.Header -- internalized errors;
wenzelm
parents:
48638
diff
changeset
|
12 |
imports: string list, |
48874
ff9cd47be39b
refined Thy_Load.check_thy: find more uses in body text, based on keywords;
wenzelm
parents:
48864
diff
changeset
|
13 |
keywords: keywords, |
46938
cda018294515
some support for outer syntax keyword declarations within theory header;
wenzelm
parents:
46737
diff
changeset
|
14 |
uses: (Path.T * bool) list} |
48874
ff9cd47be39b
refined Thy_Load.check_thy: find more uses in body text, based on keywords;
wenzelm
parents:
48864
diff
changeset
|
15 |
val make: string -> string list -> keywords -> (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
|
16 |
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
|
17 |
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
|
18 |
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
|
19 |
val args: header parser |
cda018294515
some support for outer syntax keyword declarations within theory header;
wenzelm
parents:
46737
diff
changeset
|
20 |
val read: Position.T -> string -> header |
22106 | 21 |
end; |
22 |
||
32466 | 23 |
structure Thy_Header: THY_HEADER = |
22106 | 24 |
struct |
25 |
||
48874
ff9cd47be39b
refined Thy_Load.check_thy: find more uses in body text, based on keywords;
wenzelm
parents:
48864
diff
changeset
|
26 |
type keywords = (string * Keyword.spec option) list; |
ff9cd47be39b
refined Thy_Load.check_thy: find more uses in body text, based on keywords;
wenzelm
parents:
48864
diff
changeset
|
27 |
|
46938
cda018294515
some support for outer syntax keyword declarations within theory header;
wenzelm
parents:
46737
diff
changeset
|
28 |
type header = |
48707
ba531af91148
simplified Document.Node.Header -- internalized errors;
wenzelm
parents:
48638
diff
changeset
|
29 |
{name: string, |
ba531af91148
simplified Document.Node.Header -- internalized errors;
wenzelm
parents:
48638
diff
changeset
|
30 |
imports: string list, |
48874
ff9cd47be39b
refined Thy_Load.check_thy: find more uses in body text, based on keywords;
wenzelm
parents:
48864
diff
changeset
|
31 |
keywords: keywords, |
46938
cda018294515
some support for outer syntax keyword declarations within theory header;
wenzelm
parents:
46737
diff
changeset
|
32 |
uses: (Path.T * bool) list}; |
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 |
fun make name imports keywords uses : header = |
cda018294515
some support for outer syntax keyword declarations within theory header;
wenzelm
parents:
46737
diff
changeset
|
35 |
{name = name, imports = imports, keywords = keywords, uses = uses}; |
cda018294515
some support for outer syntax keyword declarations within theory header;
wenzelm
parents:
46737
diff
changeset
|
36 |
|
cda018294515
some support for outer syntax keyword declarations within theory header;
wenzelm
parents:
46737
diff
changeset
|
37 |
|
cda018294515
some support for outer syntax keyword declarations within theory header;
wenzelm
parents:
46737
diff
changeset
|
38 |
|
cda018294515
some support for outer syntax keyword declarations within theory header;
wenzelm
parents:
46737
diff
changeset
|
39 |
(** keyword declarations **) |
cda018294515
some support for outer syntax keyword declarations within theory header;
wenzelm
parents:
46737
diff
changeset
|
40 |
|
46958
0ec8f04e753a
define keywords early when processing the theory header, before running the body commands;
wenzelm
parents:
46950
diff
changeset
|
41 |
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
|
42 |
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
|
43 |
|
48864
3ee314ae1e0a
added keyword kind "thy_load" (with optional list of file extensions);
wenzelm
parents:
48707
diff
changeset
|
44 |
fun err_dup name = error ("Duplicate declaration of outer syntax keyword " ^ quote name); |
46938
cda018294515
some support for outer syntax keyword declarations within theory header;
wenzelm
parents:
46737
diff
changeset
|
45 |
|
cda018294515
some support for outer syntax keyword declarations within theory header;
wenzelm
parents:
46737
diff
changeset
|
46 |
structure Data = Theory_Data |
cda018294515
some support for outer syntax keyword declarations within theory header;
wenzelm
parents:
46737
diff
changeset
|
47 |
( |
46961
5c6955f487e5
outer syntax command definitions based on formal command_spec derived from theory header declarations;
wenzelm
parents:
46958
diff
changeset
|
48 |
type T = Keyword.spec option Symtab.table; |
46938
cda018294515
some support for outer syntax keyword declarations within theory header;
wenzelm
parents:
46737
diff
changeset
|
49 |
val empty = Symtab.empty; |
cda018294515
some support for outer syntax keyword declarations within theory header;
wenzelm
parents:
46737
diff
changeset
|
50 |
val extend = I; |
cda018294515
some support for outer syntax keyword declarations within theory header;
wenzelm
parents:
46737
diff
changeset
|
51 |
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
|
52 |
); |
cda018294515
some support for outer syntax keyword declarations within theory header;
wenzelm
parents:
46737
diff
changeset
|
53 |
|
46961
5c6955f487e5
outer syntax command definitions based on formal command_spec derived from theory header declarations;
wenzelm
parents:
46958
diff
changeset
|
54 |
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
|
55 |
Data.map (fn data => |
5c6955f487e5
outer syntax command definitions based on formal command_spec derived from theory header declarations;
wenzelm
parents:
46958
diff
changeset
|
56 |
(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
|
57 |
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
|
58 |
|
cda018294515
some support for outer syntax keyword declarations within theory header;
wenzelm
parents:
46737
diff
changeset
|
59 |
fun the_keyword thy name = |
cda018294515
some support for outer syntax keyword declarations within theory header;
wenzelm
parents:
46737
diff
changeset
|
60 |
(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
|
61 |
SOME spec => spec |
5c6955f487e5
outer syntax command definitions based on formal command_spec derived from theory header declarations;
wenzelm
parents:
46958
diff
changeset
|
62 |
| 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
|
63 |
|
cda018294515
some support for outer syntax keyword declarations within theory header;
wenzelm
parents:
46737
diff
changeset
|
64 |
|
cda018294515
some support for outer syntax keyword declarations within theory header;
wenzelm
parents:
46737
diff
changeset
|
65 |
|
cda018294515
some support for outer syntax keyword declarations within theory header;
wenzelm
parents:
46737
diff
changeset
|
66 |
(** concrete syntax **) |
cda018294515
some support for outer syntax keyword declarations within theory header;
wenzelm
parents:
46737
diff
changeset
|
67 |
|
cda018294515
some support for outer syntax keyword declarations within theory header;
wenzelm
parents:
46737
diff
changeset
|
68 |
(* header keywords *) |
22106 | 69 |
|
70 |
val headerN = "header"; |
|
71 |
val theoryN = "theory"; |
|
72 |
val importsN = "imports"; |
|
46938
cda018294515
some support for outer syntax keyword declarations within theory header;
wenzelm
parents:
46737
diff
changeset
|
73 |
val keywordsN = "keywords"; |
22106 | 74 |
val usesN = "uses"; |
75 |
val beginN = "begin"; |
|
76 |
||
46938
cda018294515
some support for outer syntax keyword declarations within theory header;
wenzelm
parents:
46737
diff
changeset
|
77 |
val header_lexicon = |
cda018294515
some support for outer syntax keyword declarations within theory header;
wenzelm
parents:
46737
diff
changeset
|
78 |
Scan.make_lexicon |
cda018294515
some support for outer syntax keyword declarations within theory header;
wenzelm
parents:
46737
diff
changeset
|
79 |
(map Symbol.explode |
48864
3ee314ae1e0a
added keyword kind "thy_load" (with optional list of file extensions);
wenzelm
parents:
48707
diff
changeset
|
80 |
["%", "(", ")", ",", "::", ";", "and", beginN, headerN, importsN, keywordsN, theoryN, usesN]); |
22106 | 81 |
|
82 |
||
83 |
(* header args *) |
|
84 |
||
46938
cda018294515
some support for outer syntax keyword declarations within theory header;
wenzelm
parents:
46737
diff
changeset
|
85 |
local |
cda018294515
some support for outer syntax keyword declarations within theory header;
wenzelm
parents:
46737
diff
changeset
|
86 |
|
48881
46e053eda5dd
clarified Parse.path vs. Parse.explode -- prefer errors in proper transaction context;
wenzelm
parents:
48874
diff
changeset
|
87 |
val file_name = Parse.group (fn () => "file name") Parse.path >> Path.explode; |
44357 | 88 |
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
|
89 |
|
48864
3ee314ae1e0a
added keyword kind "thy_load" (with optional list of file extensions);
wenzelm
parents:
48707
diff
changeset
|
90 |
val opt_files = |
3ee314ae1e0a
added keyword kind "thy_load" (with optional list of file extensions);
wenzelm
parents:
48707
diff
changeset
|
91 |
Scan.optional (Parse.$$$ "(" |-- Parse.!!! (Parse.list1 Parse.name) --| Parse.$$$ ")") []; |
3ee314ae1e0a
added keyword kind "thy_load" (with optional list of file extensions);
wenzelm
parents:
48707
diff
changeset
|
92 |
val keyword_spec = |
3ee314ae1e0a
added keyword kind "thy_load" (with optional list of file extensions);
wenzelm
parents:
48707
diff
changeset
|
93 |
Parse.group (fn () => "outer syntax keyword specification") |
3ee314ae1e0a
added keyword kind "thy_load" (with optional list of file extensions);
wenzelm
parents:
48707
diff
changeset
|
94 |
(Parse.name -- opt_files -- Parse.tags); |
3ee314ae1e0a
added keyword kind "thy_load" (with optional list of file extensions);
wenzelm
parents:
48707
diff
changeset
|
95 |
|
46939 | 96 |
val keyword_decl = |
48864
3ee314ae1e0a
added keyword kind "thy_load" (with optional list of file extensions);
wenzelm
parents:
48707
diff
changeset
|
97 |
Scan.repeat1 Parse.string -- Scan.option (Parse.$$$ "::" |-- Parse.!!! keyword_spec) >> |
3ee314ae1e0a
added keyword kind "thy_load" (with optional list of file extensions);
wenzelm
parents:
48707
diff
changeset
|
98 |
(fn (names, spec) => map (rpair spec) names); |
46939 | 99 |
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
|
100 |
|
36950 | 101 |
val file = |
102 |
Parse.$$$ "(" |-- Parse.!!! (file_name --| Parse.$$$ ")") >> rpair false || |
|
103 |
file_name >> rpair true; |
|
104 |
||
46938
cda018294515
some support for outer syntax keyword declarations within theory header;
wenzelm
parents:
46737
diff
changeset
|
105 |
in |
22106 | 106 |
|
107 |
val args = |
|
46938
cda018294515
some support for outer syntax keyword declarations within theory header;
wenzelm
parents:
46737
diff
changeset
|
108 |
theory_name -- |
48638 | 109 |
Scan.optional (Parse.$$$ importsN |-- Parse.!!! (Scan.repeat1 theory_name)) [] -- |
46939 | 110 |
Scan.optional (Parse.$$$ keywordsN |-- Parse.!!! keyword_decls) [] -- |
46938
cda018294515
some support for outer syntax keyword declarations within theory header;
wenzelm
parents:
46737
diff
changeset
|
111 |
Scan.optional (Parse.$$$ usesN |-- Parse.!!! (Scan.repeat1 file)) [] --| |
cda018294515
some support for outer syntax keyword declarations within theory header;
wenzelm
parents:
46737
diff
changeset
|
112 |
Parse.$$$ beginN >> |
cda018294515
some support for outer syntax keyword declarations within theory header;
wenzelm
parents:
46737
diff
changeset
|
113 |
(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
|
114 |
|
cda018294515
some support for outer syntax keyword declarations within theory header;
wenzelm
parents:
46737
diff
changeset
|
115 |
end; |
22106 | 116 |
|
117 |
||
118 |
(* read header *) |
|
119 |
||
120 |
val header = |
|
36950 | 121 |
(Parse.$$$ headerN -- Parse.tags) |-- |
122 |
(Parse.!!! (Parse.doc_source -- Scan.repeat Parse.semicolon -- |
|
123 |
(Parse.$$$ theoryN -- Parse.tags) |-- args)) || |
|
124 |
(Parse.$$$ theoryN -- Parse.tags) |-- Parse.!!! args; |
|
22106 | 125 |
|
37978
548f3f165d05
simplified Thy_Header.read -- include Source.of_string_limited here;
wenzelm
parents:
37950
diff
changeset
|
126 |
fun read pos str = |
22106 | 127 |
let val res = |
37978
548f3f165d05
simplified Thy_Header.read -- include Source.of_string_limited here;
wenzelm
parents:
37950
diff
changeset
|
128 |
str |
548f3f165d05
simplified Thy_Header.read -- include Source.of_string_limited here;
wenzelm
parents:
37950
diff
changeset
|
129 |
|> 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
|
130 |
|> 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
|
131 |
|> 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
|
132 |
|> 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
|
133 |
|> Source.source Token.stopper (Scan.single (Scan.error (Parse.!!! header))) NONE |
22106 | 134 |
|> Source.get_single; |
135 |
in |
|
42003
6e45dc518ebb
replaced File.check by specific File.check_file, File.check_dir;
wenzelm
parents:
41944
diff
changeset
|
136 |
(case res of |
46938
cda018294515
some support for outer syntax keyword declarations within theory header;
wenzelm
parents:
46737
diff
changeset
|
137 |
SOME (h, _) => h |
22106 | 138 |
| NONE => error ("Unexpected end of input" ^ Position.str_of pos)) |
139 |
end; |
|
140 |
||
141 |
end; |