author | wenzelm |
Wed, 27 Feb 2013 12:45:19 +0100 | |
changeset 51293 | 05b1bbae748d |
parent 50128 | 599c935aac82 |
child 51294 | 0850d43cb355 |
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 = |
48927
ef462b5558eb
theory def/ref position reports, which enable hyperlinks etc.;
wenzelm
parents:
48881
diff
changeset
|
11 |
{name: string * Position.T, |
ef462b5558eb
theory def/ref position reports, which enable hyperlinks etc.;
wenzelm
parents:
48881
diff
changeset
|
12 |
imports: (string * Position.T) 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, |
51293
05b1bbae748d
discontinued obsolete 'uses' within theory header;
wenzelm
parents:
50128
diff
changeset
|
14 |
files: Path.T list} |
05b1bbae748d
discontinued obsolete 'uses' within theory header;
wenzelm
parents:
50128
diff
changeset
|
15 |
val make: string * Position.T -> (string * Position.T) list -> keywords -> Path.T 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 |
48927
ef462b5558eb
theory def/ref position reports, which enable hyperlinks etc.;
wenzelm
parents:
48881
diff
changeset
|
21 |
val read_tokens: Token.T list -> header |
22106 | 22 |
end; |
23 |
||
32466 | 24 |
structure Thy_Header: THY_HEADER = |
22106 | 25 |
struct |
26 |
||
48874
ff9cd47be39b
refined Thy_Load.check_thy: find more uses in body text, based on keywords;
wenzelm
parents:
48864
diff
changeset
|
27 |
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
|
28 |
|
46938
cda018294515
some support for outer syntax keyword declarations within theory header;
wenzelm
parents:
46737
diff
changeset
|
29 |
type header = |
48927
ef462b5558eb
theory def/ref position reports, which enable hyperlinks etc.;
wenzelm
parents:
48881
diff
changeset
|
30 |
{name: string * Position.T, |
ef462b5558eb
theory def/ref position reports, which enable hyperlinks etc.;
wenzelm
parents:
48881
diff
changeset
|
31 |
imports: (string * Position.T) list, |
48874
ff9cd47be39b
refined Thy_Load.check_thy: find more uses in body text, based on keywords;
wenzelm
parents:
48864
diff
changeset
|
32 |
keywords: keywords, |
51293
05b1bbae748d
discontinued obsolete 'uses' within theory header;
wenzelm
parents:
50128
diff
changeset
|
33 |
files: Path.T list}; |
46938
cda018294515
some support for outer syntax keyword declarations within theory header;
wenzelm
parents:
46737
diff
changeset
|
34 |
|
51293
05b1bbae748d
discontinued obsolete 'uses' within theory header;
wenzelm
parents:
50128
diff
changeset
|
35 |
fun make name imports keywords files : header = |
05b1bbae748d
discontinued obsolete 'uses' within theory header;
wenzelm
parents:
50128
diff
changeset
|
36 |
{name = name, imports = imports, keywords = keywords, files = files}; |
46938
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 |
|
cda018294515
some support for outer syntax keyword declarations within theory header;
wenzelm
parents:
46737
diff
changeset
|
40 |
(** keyword declarations **) |
cda018294515
some support for outer syntax keyword declarations within theory header;
wenzelm
parents:
46737
diff
changeset
|
41 |
|
46958
0ec8f04e753a
define keywords early when processing the theory header, before running the body commands;
wenzelm
parents:
46950
diff
changeset
|
42 |
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
|
43 |
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
|
44 |
|
48864
3ee314ae1e0a
added keyword kind "thy_load" (with optional list of file extensions);
wenzelm
parents:
48707
diff
changeset
|
45 |
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
|
46 |
|
cda018294515
some support for outer syntax keyword declarations within theory header;
wenzelm
parents:
46737
diff
changeset
|
47 |
structure Data = Theory_Data |
cda018294515
some support for outer syntax keyword declarations within theory header;
wenzelm
parents:
46737
diff
changeset
|
48 |
( |
46961
5c6955f487e5
outer syntax command definitions based on formal command_spec derived from theory header declarations;
wenzelm
parents:
46958
diff
changeset
|
49 |
type T = Keyword.spec option Symtab.table; |
46938
cda018294515
some support for outer syntax keyword declarations within theory header;
wenzelm
parents:
46737
diff
changeset
|
50 |
val empty = Symtab.empty; |
cda018294515
some support for outer syntax keyword declarations within theory header;
wenzelm
parents:
46737
diff
changeset
|
51 |
val extend = I; |
cda018294515
some support for outer syntax keyword declarations within theory header;
wenzelm
parents:
46737
diff
changeset
|
52 |
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
|
53 |
); |
cda018294515
some support for outer syntax keyword declarations within theory header;
wenzelm
parents:
46737
diff
changeset
|
54 |
|
46961
5c6955f487e5
outer syntax command definitions based on formal command_spec derived from theory header declarations;
wenzelm
parents:
46958
diff
changeset
|
55 |
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
|
56 |
Data.map (fn data => |
5c6955f487e5
outer syntax command definitions based on formal command_spec derived from theory header declarations;
wenzelm
parents:
46958
diff
changeset
|
57 |
(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
|
58 |
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
|
59 |
|
cda018294515
some support for outer syntax keyword declarations within theory header;
wenzelm
parents:
46737
diff
changeset
|
60 |
fun the_keyword thy name = |
cda018294515
some support for outer syntax keyword declarations within theory header;
wenzelm
parents:
46737
diff
changeset
|
61 |
(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
|
62 |
SOME spec => spec |
5c6955f487e5
outer syntax command definitions based on formal command_spec derived from theory header declarations;
wenzelm
parents:
46958
diff
changeset
|
63 |
| 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
|
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 |
|
cda018294515
some support for outer syntax keyword declarations within theory header;
wenzelm
parents:
46737
diff
changeset
|
67 |
(** concrete syntax **) |
cda018294515
some support for outer syntax keyword declarations within theory header;
wenzelm
parents:
46737
diff
changeset
|
68 |
|
cda018294515
some support for outer syntax keyword declarations within theory header;
wenzelm
parents:
46737
diff
changeset
|
69 |
(* header keywords *) |
22106 | 70 |
|
71 |
val headerN = "header"; |
|
72 |
val theoryN = "theory"; |
|
73 |
val importsN = "imports"; |
|
46938
cda018294515
some support for outer syntax keyword declarations within theory header;
wenzelm
parents:
46737
diff
changeset
|
74 |
val keywordsN = "keywords"; |
22106 | 75 |
val beginN = "begin"; |
76 |
||
48927
ef462b5558eb
theory def/ref position reports, which enable hyperlinks etc.;
wenzelm
parents:
48881
diff
changeset
|
77 |
val header_lexicons = |
ef462b5558eb
theory def/ref position reports, which enable hyperlinks etc.;
wenzelm
parents:
48881
diff
changeset
|
78 |
pairself (Scan.make_lexicon o map Symbol.explode) |
51293
05b1bbae748d
discontinued obsolete 'uses' within theory header;
wenzelm
parents:
50128
diff
changeset
|
79 |
(["%", "(", ")", ",", "::", ";", "==", "and", beginN, importsN, keywordsN], |
48927
ef462b5558eb
theory def/ref position reports, which enable hyperlinks etc.;
wenzelm
parents:
48881
diff
changeset
|
80 |
[headerN, theoryN]); |
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 |
|
48927
ef462b5558eb
theory def/ref position reports, which enable hyperlinks etc.;
wenzelm
parents:
48881
diff
changeset
|
87 |
val theory_name = Parse.group (fn () => "theory name") (Parse.position Parse.name); |
27890
62ac62e30ab1
args: explicit groups for file_name, theory_name;
wenzelm
parents:
27872
diff
changeset
|
88 |
|
48864
3ee314ae1e0a
added keyword kind "thy_load" (with optional list of file extensions);
wenzelm
parents:
48707
diff
changeset
|
89 |
val opt_files = |
3ee314ae1e0a
added keyword kind "thy_load" (with optional list of file extensions);
wenzelm
parents:
48707
diff
changeset
|
90 |
Scan.optional (Parse.$$$ "(" |-- Parse.!!! (Parse.list1 Parse.name) --| Parse.$$$ ")") []; |
50128
599c935aac82
alternative completion for outer syntax keywords;
wenzelm
parents:
48992
diff
changeset
|
91 |
|
48864
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 |
|
50128
599c935aac82
alternative completion for outer syntax keywords;
wenzelm
parents:
48992
diff
changeset
|
96 |
val keyword_compl = |
599c935aac82
alternative completion for outer syntax keywords;
wenzelm
parents:
48992
diff
changeset
|
97 |
Parse.group (fn () => "outer syntax keyword completion") Parse.name; |
599c935aac82
alternative completion for outer syntax keywords;
wenzelm
parents:
48992
diff
changeset
|
98 |
|
46939 | 99 |
val keyword_decl = |
50128
599c935aac82
alternative completion for outer syntax keywords;
wenzelm
parents:
48992
diff
changeset
|
100 |
Scan.repeat1 Parse.string -- |
599c935aac82
alternative completion for outer syntax keywords;
wenzelm
parents:
48992
diff
changeset
|
101 |
Scan.option (Parse.$$$ "::" |-- Parse.!!! keyword_spec) -- |
599c935aac82
alternative completion for outer syntax keywords;
wenzelm
parents:
48992
diff
changeset
|
102 |
Scan.option (Parse.$$$ "==" |-- Parse.!!! keyword_compl) |
599c935aac82
alternative completion for outer syntax keywords;
wenzelm
parents:
48992
diff
changeset
|
103 |
>> (fn ((names, spec), _) => map (rpair spec) names); |
599c935aac82
alternative completion for outer syntax keywords;
wenzelm
parents:
48992
diff
changeset
|
104 |
|
46939 | 105 |
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
|
106 |
|
cda018294515
some support for outer syntax keyword declarations within theory header;
wenzelm
parents:
46737
diff
changeset
|
107 |
in |
22106 | 108 |
|
109 |
val args = |
|
46938
cda018294515
some support for outer syntax keyword declarations within theory header;
wenzelm
parents:
46737
diff
changeset
|
110 |
theory_name -- |
48638 | 111 |
Scan.optional (Parse.$$$ importsN |-- Parse.!!! (Scan.repeat1 theory_name)) [] -- |
51293
05b1bbae748d
discontinued obsolete 'uses' within theory header;
wenzelm
parents:
50128
diff
changeset
|
112 |
Scan.optional (Parse.$$$ keywordsN |-- Parse.!!! keyword_decls) [] --| |
46938
cda018294515
some support for outer syntax keyword declarations within theory header;
wenzelm
parents:
46737
diff
changeset
|
113 |
Parse.$$$ beginN >> |
51293
05b1bbae748d
discontinued obsolete 'uses' within theory header;
wenzelm
parents:
50128
diff
changeset
|
114 |
(fn ((name, imports), keywords) => make name imports keywords []); |
46938
cda018294515
some support for outer syntax keyword declarations within theory header;
wenzelm
parents:
46737
diff
changeset
|
115 |
|
cda018294515
some support for outer syntax keyword declarations within theory header;
wenzelm
parents:
46737
diff
changeset
|
116 |
end; |
22106 | 117 |
|
118 |
||
119 |
(* read header *) |
|
120 |
||
121 |
val header = |
|
48927
ef462b5558eb
theory def/ref position reports, which enable hyperlinks etc.;
wenzelm
parents:
48881
diff
changeset
|
122 |
(Parse.command_name headerN -- Parse.tags) |-- |
36950 | 123 |
(Parse.!!! (Parse.doc_source -- Scan.repeat Parse.semicolon -- |
48927
ef462b5558eb
theory def/ref position reports, which enable hyperlinks etc.;
wenzelm
parents:
48881
diff
changeset
|
124 |
(Parse.command_name theoryN -- Parse.tags) |-- args)) || |
ef462b5558eb
theory def/ref position reports, which enable hyperlinks etc.;
wenzelm
parents:
48881
diff
changeset
|
125 |
(Parse.command_name theoryN -- Parse.tags) |-- Parse.!!! args; |
22106 | 126 |
|
48927
ef462b5558eb
theory def/ref position reports, which enable hyperlinks etc.;
wenzelm
parents:
48881
diff
changeset
|
127 |
fun token_source pos str = |
ef462b5558eb
theory def/ref position reports, which enable hyperlinks etc.;
wenzelm
parents:
48881
diff
changeset
|
128 |
str |
ef462b5558eb
theory def/ref position reports, which enable hyperlinks etc.;
wenzelm
parents:
48881
diff
changeset
|
129 |
|> Source.of_string_limited 8000 |
ef462b5558eb
theory def/ref position reports, which enable hyperlinks etc.;
wenzelm
parents:
48881
diff
changeset
|
130 |
|> Symbol.source |
ef462b5558eb
theory def/ref position reports, which enable hyperlinks etc.;
wenzelm
parents:
48881
diff
changeset
|
131 |
|> Token.source {do_recover = NONE} (K header_lexicons) pos; |
ef462b5558eb
theory def/ref position reports, which enable hyperlinks etc.;
wenzelm
parents:
48881
diff
changeset
|
132 |
|
ef462b5558eb
theory def/ref position reports, which enable hyperlinks etc.;
wenzelm
parents:
48881
diff
changeset
|
133 |
fun read_source pos source = |
22106 | 134 |
let val res = |
48927
ef462b5558eb
theory def/ref position reports, which enable hyperlinks etc.;
wenzelm
parents:
48881
diff
changeset
|
135 |
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
|
136 |
|> 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
|
137 |
|> Source.source Token.stopper (Scan.single (Scan.error (Parse.!!! header))) NONE |
22106 | 138 |
|> Source.get_single; |
139 |
in |
|
42003
6e45dc518ebb
replaced File.check by specific File.check_file, File.check_dir;
wenzelm
parents:
41944
diff
changeset
|
140 |
(case res of |
46938
cda018294515
some support for outer syntax keyword declarations within theory header;
wenzelm
parents:
46737
diff
changeset
|
141 |
SOME (h, _) => h |
48992 | 142 |
| NONE => error ("Unexpected end of input" ^ Position.here pos)) |
22106 | 143 |
end; |
144 |
||
48927
ef462b5558eb
theory def/ref position reports, which enable hyperlinks etc.;
wenzelm
parents:
48881
diff
changeset
|
145 |
fun read pos str = read_source pos (token_source pos str); |
ef462b5558eb
theory def/ref position reports, which enable hyperlinks etc.;
wenzelm
parents:
48881
diff
changeset
|
146 |
fun read_tokens toks = read_source Position.none (Source.of_list toks); |
ef462b5558eb
theory def/ref position reports, which enable hyperlinks etc.;
wenzelm
parents:
48881
diff
changeset
|
147 |
|
22106 | 148 |
end; |