author | wenzelm |
Fri, 16 Mar 2012 18:20:12 +0100 | |
changeset 46961 | 5c6955f487e5 |
parent 46958 | 0ec8f04e753a |
child 46967 | 499d9bbd8de9 |
permissions | -rw-r--r-- |
36949
080e85d46108
renamed structure OuterKeyword to Keyword and OuterParse to Parse, keeping the old names as legacy aliases for some time;
wenzelm
parents:
36681
diff
changeset
|
1 |
(* Title: Pure/Isar/keyword.ML |
17059
a001a3ebfcfd
Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff
changeset
|
2 |
Author: Makarius |
a001a3ebfcfd
Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff
changeset
|
3 |
|
27357
5b3a087ff292
moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents:
17270
diff
changeset
|
4 |
Isar command keyword classification and global keyword tables. |
17059
a001a3ebfcfd
Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff
changeset
|
5 |
*) |
a001a3ebfcfd
Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff
changeset
|
6 |
|
36949
080e85d46108
renamed structure OuterKeyword to Keyword and OuterParse to Parse, keeping the old names as legacy aliases for some time;
wenzelm
parents:
36681
diff
changeset
|
7 |
signature KEYWORD = |
17059
a001a3ebfcfd
Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff
changeset
|
8 |
sig |
a001a3ebfcfd
Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff
changeset
|
9 |
type T |
a001a3ebfcfd
Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff
changeset
|
10 |
val kind_of: T -> string |
a001a3ebfcfd
Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff
changeset
|
11 |
val control: T |
a001a3ebfcfd
Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff
changeset
|
12 |
val diag: T |
a001a3ebfcfd
Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff
changeset
|
13 |
val thy_begin: T |
a001a3ebfcfd
Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff
changeset
|
14 |
val thy_switch: T |
a001a3ebfcfd
Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff
changeset
|
15 |
val thy_end: T |
a001a3ebfcfd
Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff
changeset
|
16 |
val thy_heading: T |
a001a3ebfcfd
Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff
changeset
|
17 |
val thy_decl: T |
a001a3ebfcfd
Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff
changeset
|
18 |
val thy_script: T |
a001a3ebfcfd
Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff
changeset
|
19 |
val thy_goal: T |
36315
e859879079c8
added keyword category "schematic goal", which prevents any attempt to fork the proof;
wenzelm
parents:
34243
diff
changeset
|
20 |
val thy_schematic_goal: T |
17059
a001a3ebfcfd
Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff
changeset
|
21 |
val qed: T |
a001a3ebfcfd
Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff
changeset
|
22 |
val qed_block: T |
a001a3ebfcfd
Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff
changeset
|
23 |
val qed_global: T |
a001a3ebfcfd
Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff
changeset
|
24 |
val prf_heading: T |
a001a3ebfcfd
Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff
changeset
|
25 |
val prf_goal: T |
a001a3ebfcfd
Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff
changeset
|
26 |
val prf_block: T |
a001a3ebfcfd
Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff
changeset
|
27 |
val prf_open: T |
a001a3ebfcfd
Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff
changeset
|
28 |
val prf_close: T |
a001a3ebfcfd
Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff
changeset
|
29 |
val prf_chain: T |
a001a3ebfcfd
Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff
changeset
|
30 |
val prf_decl: T |
a001a3ebfcfd
Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff
changeset
|
31 |
val prf_asm: T |
a001a3ebfcfd
Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff
changeset
|
32 |
val prf_asm_goal: T |
a001a3ebfcfd
Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff
changeset
|
33 |
val prf_script: T |
a001a3ebfcfd
Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff
changeset
|
34 |
val kinds: string list |
a001a3ebfcfd
Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff
changeset
|
35 |
val tag: string -> T -> T |
a001a3ebfcfd
Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff
changeset
|
36 |
val tags_of: T -> string list |
a001a3ebfcfd
Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff
changeset
|
37 |
val tag_theory: T -> T |
a001a3ebfcfd
Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff
changeset
|
38 |
val tag_proof: T -> T |
a001a3ebfcfd
Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff
changeset
|
39 |
val tag_ml: T -> T |
46961
5c6955f487e5
outer syntax command definitions based on formal command_spec derived from theory header declarations;
wenzelm
parents:
46958
diff
changeset
|
40 |
type spec = string * string list |
5c6955f487e5
outer syntax command definitions based on formal command_spec derived from theory header declarations;
wenzelm
parents:
46958
diff
changeset
|
41 |
val spec: spec -> T |
5c6955f487e5
outer syntax command definitions based on formal command_spec derived from theory header declarations;
wenzelm
parents:
46958
diff
changeset
|
42 |
val command_spec: string * spec -> string * T |
27357
5b3a087ff292
moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents:
17270
diff
changeset
|
43 |
val get_lexicons: unit -> Scan.lexicon * Scan.lexicon |
5b3a087ff292
moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents:
17270
diff
changeset
|
44 |
val is_keyword: string -> bool |
5b3a087ff292
moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents:
17270
diff
changeset
|
45 |
val command_keyword: string -> T option |
5b3a087ff292
moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents:
17270
diff
changeset
|
46 |
val command_tags: string -> string list |
46957
0c15caf47040
clarified Keyword.is_keyword: union of minor and major;
wenzelm
parents:
46950
diff
changeset
|
47 |
val dest: unit -> string list * string list |
38236
d8c7be27e01d
explicitly distinguish Output.status (essential feedback) vs. Output.report (useful markup);
wenzelm
parents:
36955
diff
changeset
|
48 |
val keyword_statusN: string |
d8c7be27e01d
explicitly distinguish Output.status (essential feedback) vs. Output.report (useful markup);
wenzelm
parents:
36955
diff
changeset
|
49 |
val status: unit -> unit |
46958
0ec8f04e753a
define keywords early when processing the theory header, before running the body commands;
wenzelm
parents:
46957
diff
changeset
|
50 |
val define: string * T option -> unit |
29347 | 51 |
val is_diag: string -> bool |
52 |
val is_control: string -> bool |
|
53 |
val is_regular: string -> bool |
|
40397 | 54 |
val is_heading: string -> bool |
29347 | 55 |
val is_theory_begin: string -> bool |
27440
a1eda23752bd
replaced datatype category constructivism by is_theory/is_proof;
wenzelm
parents:
27433
diff
changeset
|
56 |
val is_theory: string -> bool |
a1eda23752bd
replaced datatype category constructivism by is_theory/is_proof;
wenzelm
parents:
27433
diff
changeset
|
57 |
val is_proof: string -> bool |
28431 | 58 |
val is_theory_goal: string -> bool |
59 |
val is_proof_goal: string -> bool |
|
36315
e859879079c8
added keyword category "schematic goal", which prevents any attempt to fork the proof;
wenzelm
parents:
34243
diff
changeset
|
60 |
val is_schematic_goal: string -> bool |
28431 | 61 |
val is_qed: string -> bool |
62 |
val is_qed_global: string -> bool |
|
17059
a001a3ebfcfd
Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff
changeset
|
63 |
end; |
a001a3ebfcfd
Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff
changeset
|
64 |
|
36949
080e85d46108
renamed structure OuterKeyword to Keyword and OuterParse to Parse, keeping the old names as legacy aliases for some time;
wenzelm
parents:
36681
diff
changeset
|
65 |
structure Keyword: KEYWORD = |
17059
a001a3ebfcfd
Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff
changeset
|
66 |
struct |
a001a3ebfcfd
Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff
changeset
|
67 |
|
27357
5b3a087ff292
moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents:
17270
diff
changeset
|
68 |
(** keyword classification **) |
17059
a001a3ebfcfd
Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff
changeset
|
69 |
|
46961
5c6955f487e5
outer syntax command definitions based on formal command_spec derived from theory header declarations;
wenzelm
parents:
46958
diff
changeset
|
70 |
datatype T = Keyword of string * string list; (*kind, tags (in canonical reverse order)*) |
17059
a001a3ebfcfd
Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff
changeset
|
71 |
|
a001a3ebfcfd
Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff
changeset
|
72 |
fun kind s = Keyword (s, []); |
a001a3ebfcfd
Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff
changeset
|
73 |
fun kind_of (Keyword (s, _)) = s; |
a001a3ebfcfd
Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff
changeset
|
74 |
|
a001a3ebfcfd
Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff
changeset
|
75 |
|
a001a3ebfcfd
Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff
changeset
|
76 |
(* kinds *) |
a001a3ebfcfd
Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff
changeset
|
77 |
|
a001a3ebfcfd
Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff
changeset
|
78 |
val control = kind "control"; |
a001a3ebfcfd
Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff
changeset
|
79 |
val diag = kind "diag"; |
a001a3ebfcfd
Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff
changeset
|
80 |
val thy_begin = kind "theory-begin"; |
a001a3ebfcfd
Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff
changeset
|
81 |
val thy_switch = kind "theory-switch"; |
a001a3ebfcfd
Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff
changeset
|
82 |
val thy_end = kind "theory-end"; |
a001a3ebfcfd
Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff
changeset
|
83 |
val thy_heading = kind "theory-heading"; |
a001a3ebfcfd
Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff
changeset
|
84 |
val thy_decl = kind "theory-decl"; |
a001a3ebfcfd
Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff
changeset
|
85 |
val thy_script = kind "theory-script"; |
a001a3ebfcfd
Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff
changeset
|
86 |
val thy_goal = kind "theory-goal"; |
36315
e859879079c8
added keyword category "schematic goal", which prevents any attempt to fork the proof;
wenzelm
parents:
34243
diff
changeset
|
87 |
val thy_schematic_goal = kind "theory-schematic-goal"; |
17059
a001a3ebfcfd
Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff
changeset
|
88 |
val qed = kind "qed"; |
a001a3ebfcfd
Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff
changeset
|
89 |
val qed_block = kind "qed-block"; |
a001a3ebfcfd
Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff
changeset
|
90 |
val qed_global = kind "qed-global"; |
a001a3ebfcfd
Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff
changeset
|
91 |
val prf_heading = kind "proof-heading"; |
a001a3ebfcfd
Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff
changeset
|
92 |
val prf_goal = kind "proof-goal"; |
a001a3ebfcfd
Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff
changeset
|
93 |
val prf_block = kind "proof-block"; |
a001a3ebfcfd
Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff
changeset
|
94 |
val prf_open = kind "proof-open"; |
a001a3ebfcfd
Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff
changeset
|
95 |
val prf_close = kind "proof-close"; |
a001a3ebfcfd
Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff
changeset
|
96 |
val prf_chain = kind "proof-chain"; |
a001a3ebfcfd
Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff
changeset
|
97 |
val prf_decl = kind "proof-decl"; |
a001a3ebfcfd
Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff
changeset
|
98 |
val prf_asm = kind "proof-asm"; |
a001a3ebfcfd
Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff
changeset
|
99 |
val prf_asm_goal = kind "proof-asm-goal"; |
a001a3ebfcfd
Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff
changeset
|
100 |
val prf_script = kind "proof-script"; |
a001a3ebfcfd
Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff
changeset
|
101 |
|
36315
e859879079c8
added keyword category "schematic goal", which prevents any attempt to fork the proof;
wenzelm
parents:
34243
diff
changeset
|
102 |
val kinds = |
e859879079c8
added keyword category "schematic goal", which prevents any attempt to fork the proof;
wenzelm
parents:
34243
diff
changeset
|
103 |
[control, diag, thy_begin, thy_switch, thy_end, thy_heading, thy_decl, thy_script, thy_goal, |
e859879079c8
added keyword category "schematic goal", which prevents any attempt to fork the proof;
wenzelm
parents:
34243
diff
changeset
|
104 |
thy_schematic_goal, qed, qed_block, qed_global, prf_heading, prf_goal, prf_block, prf_open, |
e859879079c8
added keyword category "schematic goal", which prevents any attempt to fork the proof;
wenzelm
parents:
34243
diff
changeset
|
105 |
prf_close, prf_chain, prf_decl, prf_asm, prf_asm_goal, prf_script] |
e859879079c8
added keyword category "schematic goal", which prevents any attempt to fork the proof;
wenzelm
parents:
34243
diff
changeset
|
106 |
|> map kind_of; |
17059
a001a3ebfcfd
Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff
changeset
|
107 |
|
a001a3ebfcfd
Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff
changeset
|
108 |
|
a001a3ebfcfd
Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff
changeset
|
109 |
(* tags *) |
a001a3ebfcfd
Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff
changeset
|
110 |
|
46924 | 111 |
fun tag t (Keyword (s, ts)) = Keyword (s, update (op =) t ts); |
17059
a001a3ebfcfd
Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff
changeset
|
112 |
fun tags_of (Keyword (_, ts)) = ts; |
a001a3ebfcfd
Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff
changeset
|
113 |
|
a001a3ebfcfd
Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff
changeset
|
114 |
val tag_theory = tag "theory"; |
a001a3ebfcfd
Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff
changeset
|
115 |
val tag_proof = tag "proof"; |
a001a3ebfcfd
Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff
changeset
|
116 |
val tag_ml = tag "ML"; |
a001a3ebfcfd
Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff
changeset
|
117 |
|
27357
5b3a087ff292
moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents:
17270
diff
changeset
|
118 |
|
46938
cda018294515
some support for outer syntax keyword declarations within theory header;
wenzelm
parents:
46924
diff
changeset
|
119 |
(* external names *) |
cda018294515
some support for outer syntax keyword declarations within theory header;
wenzelm
parents:
46924
diff
changeset
|
120 |
|
cda018294515
some support for outer syntax keyword declarations within theory header;
wenzelm
parents:
46924
diff
changeset
|
121 |
val name_table = Symtab.make |
cda018294515
some support for outer syntax keyword declarations within theory header;
wenzelm
parents:
46924
diff
changeset
|
122 |
[("control", control), |
cda018294515
some support for outer syntax keyword declarations within theory header;
wenzelm
parents:
46924
diff
changeset
|
123 |
("diag", diag), |
cda018294515
some support for outer syntax keyword declarations within theory header;
wenzelm
parents:
46924
diff
changeset
|
124 |
("thy_begin", thy_begin), |
cda018294515
some support for outer syntax keyword declarations within theory header;
wenzelm
parents:
46924
diff
changeset
|
125 |
("thy_switch", thy_switch), |
cda018294515
some support for outer syntax keyword declarations within theory header;
wenzelm
parents:
46924
diff
changeset
|
126 |
("thy_end", thy_end), |
cda018294515
some support for outer syntax keyword declarations within theory header;
wenzelm
parents:
46924
diff
changeset
|
127 |
("thy_heading", thy_heading), |
cda018294515
some support for outer syntax keyword declarations within theory header;
wenzelm
parents:
46924
diff
changeset
|
128 |
("thy_decl", thy_decl), |
cda018294515
some support for outer syntax keyword declarations within theory header;
wenzelm
parents:
46924
diff
changeset
|
129 |
("thy_script", thy_script), |
cda018294515
some support for outer syntax keyword declarations within theory header;
wenzelm
parents:
46924
diff
changeset
|
130 |
("thy_goal", thy_goal), |
cda018294515
some support for outer syntax keyword declarations within theory header;
wenzelm
parents:
46924
diff
changeset
|
131 |
("thy_schematic_goal", thy_schematic_goal), |
cda018294515
some support for outer syntax keyword declarations within theory header;
wenzelm
parents:
46924
diff
changeset
|
132 |
("qed", qed), |
cda018294515
some support for outer syntax keyword declarations within theory header;
wenzelm
parents:
46924
diff
changeset
|
133 |
("qed_block", qed_block), |
cda018294515
some support for outer syntax keyword declarations within theory header;
wenzelm
parents:
46924
diff
changeset
|
134 |
("qed_global", qed_global), |
cda018294515
some support for outer syntax keyword declarations within theory header;
wenzelm
parents:
46924
diff
changeset
|
135 |
("prf_heading", prf_heading), |
cda018294515
some support for outer syntax keyword declarations within theory header;
wenzelm
parents:
46924
diff
changeset
|
136 |
("prf_goal", prf_goal), |
cda018294515
some support for outer syntax keyword declarations within theory header;
wenzelm
parents:
46924
diff
changeset
|
137 |
("prf_block", prf_block), |
cda018294515
some support for outer syntax keyword declarations within theory header;
wenzelm
parents:
46924
diff
changeset
|
138 |
("prf_open", prf_open), |
cda018294515
some support for outer syntax keyword declarations within theory header;
wenzelm
parents:
46924
diff
changeset
|
139 |
("prf_close", prf_close), |
cda018294515
some support for outer syntax keyword declarations within theory header;
wenzelm
parents:
46924
diff
changeset
|
140 |
("prf_chain", prf_chain), |
cda018294515
some support for outer syntax keyword declarations within theory header;
wenzelm
parents:
46924
diff
changeset
|
141 |
("prf_decl", prf_decl), |
cda018294515
some support for outer syntax keyword declarations within theory header;
wenzelm
parents:
46924
diff
changeset
|
142 |
("prf_asm", prf_asm), |
cda018294515
some support for outer syntax keyword declarations within theory header;
wenzelm
parents:
46924
diff
changeset
|
143 |
("prf_asm_goal", prf_asm_goal), |
cda018294515
some support for outer syntax keyword declarations within theory header;
wenzelm
parents:
46924
diff
changeset
|
144 |
("prf_script", prf_script)]; |
cda018294515
some support for outer syntax keyword declarations within theory header;
wenzelm
parents:
46924
diff
changeset
|
145 |
|
46961
5c6955f487e5
outer syntax command definitions based on formal command_spec derived from theory header declarations;
wenzelm
parents:
46958
diff
changeset
|
146 |
type spec = string * string list; |
5c6955f487e5
outer syntax command definitions based on formal command_spec derived from theory header declarations;
wenzelm
parents:
46958
diff
changeset
|
147 |
|
5c6955f487e5
outer syntax command definitions based on formal command_spec derived from theory header declarations;
wenzelm
parents:
46958
diff
changeset
|
148 |
fun spec (kind, tags) = |
46938
cda018294515
some support for outer syntax keyword declarations within theory header;
wenzelm
parents:
46924
diff
changeset
|
149 |
(case Symtab.lookup name_table kind of |
cda018294515
some support for outer syntax keyword declarations within theory header;
wenzelm
parents:
46924
diff
changeset
|
150 |
SOME k => k |> fold tag tags |
cda018294515
some support for outer syntax keyword declarations within theory header;
wenzelm
parents:
46924
diff
changeset
|
151 |
| NONE => error ("Unknown outer syntax keyword kind " ^ quote kind)); |
cda018294515
some support for outer syntax keyword declarations within theory header;
wenzelm
parents:
46924
diff
changeset
|
152 |
|
46961
5c6955f487e5
outer syntax command definitions based on formal command_spec derived from theory header declarations;
wenzelm
parents:
46958
diff
changeset
|
153 |
fun command_spec (name, s) = (name, spec s); |
5c6955f487e5
outer syntax command definitions based on formal command_spec derived from theory header declarations;
wenzelm
parents:
46958
diff
changeset
|
154 |
|
46938
cda018294515
some support for outer syntax keyword declarations within theory header;
wenzelm
parents:
46924
diff
changeset
|
155 |
|
27357
5b3a087ff292
moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents:
17270
diff
changeset
|
156 |
|
5b3a087ff292
moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents:
17270
diff
changeset
|
157 |
(** global keyword tables **) |
5b3a087ff292
moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents:
17270
diff
changeset
|
158 |
|
46957
0c15caf47040
clarified Keyword.is_keyword: union of minor and major;
wenzelm
parents:
46950
diff
changeset
|
159 |
type keywords = |
0c15caf47040
clarified Keyword.is_keyword: union of minor and major;
wenzelm
parents:
46950
diff
changeset
|
160 |
{lexicons: Scan.lexicon * Scan.lexicon, (*minor, major*) |
0c15caf47040
clarified Keyword.is_keyword: union of minor and major;
wenzelm
parents:
46950
diff
changeset
|
161 |
commands: T Symtab.table}; (*command classification*) |
0c15caf47040
clarified Keyword.is_keyword: union of minor and major;
wenzelm
parents:
46950
diff
changeset
|
162 |
|
0c15caf47040
clarified Keyword.is_keyword: union of minor and major;
wenzelm
parents:
46950
diff
changeset
|
163 |
fun make_keywords (lexicons, commands) : keywords = |
0c15caf47040
clarified Keyword.is_keyword: union of minor and major;
wenzelm
parents:
46950
diff
changeset
|
164 |
{lexicons = lexicons, commands = commands}; |
0c15caf47040
clarified Keyword.is_keyword: union of minor and major;
wenzelm
parents:
46950
diff
changeset
|
165 |
|
27357
5b3a087ff292
moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents:
17270
diff
changeset
|
166 |
local |
5b3a087ff292
moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents:
17270
diff
changeset
|
167 |
|
46957
0c15caf47040
clarified Keyword.is_keyword: union of minor and major;
wenzelm
parents:
46950
diff
changeset
|
168 |
val global_keywords = |
0c15caf47040
clarified Keyword.is_keyword: union of minor and major;
wenzelm
parents:
46950
diff
changeset
|
169 |
Unsynchronized.ref (make_keywords ((Scan.empty_lexicon, Scan.empty_lexicon), Symtab.empty)); |
27357
5b3a087ff292
moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents:
17270
diff
changeset
|
170 |
|
5b3a087ff292
moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents:
17270
diff
changeset
|
171 |
in |
5b3a087ff292
moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents:
17270
diff
changeset
|
172 |
|
46957
0c15caf47040
clarified Keyword.is_keyword: union of minor and major;
wenzelm
parents:
46950
diff
changeset
|
173 |
fun get_keywords () = ! global_keywords; |
27357
5b3a087ff292
moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents:
17270
diff
changeset
|
174 |
|
46957
0c15caf47040
clarified Keyword.is_keyword: union of minor and major;
wenzelm
parents:
46950
diff
changeset
|
175 |
fun change_keywords f = CRITICAL (fn () => |
0c15caf47040
clarified Keyword.is_keyword: union of minor and major;
wenzelm
parents:
46950
diff
changeset
|
176 |
Unsynchronized.change global_keywords |
0c15caf47040
clarified Keyword.is_keyword: union of minor and major;
wenzelm
parents:
46950
diff
changeset
|
177 |
(fn {lexicons, commands} => make_keywords (f (lexicons, commands)))); |
27357
5b3a087ff292
moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents:
17270
diff
changeset
|
178 |
|
17059
a001a3ebfcfd
Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff
changeset
|
179 |
end; |
27357
5b3a087ff292
moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents:
17270
diff
changeset
|
180 |
|
46957
0c15caf47040
clarified Keyword.is_keyword: union of minor and major;
wenzelm
parents:
46950
diff
changeset
|
181 |
fun get_lexicons () = #lexicons (get_keywords ()); |
0c15caf47040
clarified Keyword.is_keyword: union of minor and major;
wenzelm
parents:
46950
diff
changeset
|
182 |
fun get_commands () = #commands (get_keywords ()); |
0c15caf47040
clarified Keyword.is_keyword: union of minor and major;
wenzelm
parents:
46950
diff
changeset
|
183 |
|
27357
5b3a087ff292
moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents:
17270
diff
changeset
|
184 |
|
5b3a087ff292
moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents:
17270
diff
changeset
|
185 |
(* lookup *) |
5b3a087ff292
moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents:
17270
diff
changeset
|
186 |
|
46957
0c15caf47040
clarified Keyword.is_keyword: union of minor and major;
wenzelm
parents:
46950
diff
changeset
|
187 |
fun is_keyword s = |
0c15caf47040
clarified Keyword.is_keyword: union of minor and major;
wenzelm
parents:
46950
diff
changeset
|
188 |
let |
0c15caf47040
clarified Keyword.is_keyword: union of minor and major;
wenzelm
parents:
46950
diff
changeset
|
189 |
val (minor, major) = get_lexicons (); |
0c15caf47040
clarified Keyword.is_keyword: union of minor and major;
wenzelm
parents:
46950
diff
changeset
|
190 |
val syms = Symbol.explode s; |
0c15caf47040
clarified Keyword.is_keyword: union of minor and major;
wenzelm
parents:
46950
diff
changeset
|
191 |
in Scan.is_literal minor syms orelse Scan.is_literal major syms end; |
27357
5b3a087ff292
moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents:
17270
diff
changeset
|
192 |
|
5b3a087ff292
moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents:
17270
diff
changeset
|
193 |
fun command_keyword name = Symtab.lookup (get_commands ()) name; |
5b3a087ff292
moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents:
17270
diff
changeset
|
194 |
fun command_tags name = these (Option.map tags_of (command_keyword name)); |
5b3a087ff292
moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents:
17270
diff
changeset
|
195 |
|
46957
0c15caf47040
clarified Keyword.is_keyword: union of minor and major;
wenzelm
parents:
46950
diff
changeset
|
196 |
fun dest () = pairself (sort_strings o Scan.dest_lexicon) (get_lexicons ()); |
0c15caf47040
clarified Keyword.is_keyword: union of minor and major;
wenzelm
parents:
46950
diff
changeset
|
197 |
|
27357
5b3a087ff292
moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents:
17270
diff
changeset
|
198 |
|
38236
d8c7be27e01d
explicitly distinguish Output.status (essential feedback) vs. Output.report (useful markup);
wenzelm
parents:
36955
diff
changeset
|
199 |
(* status *) |
27357
5b3a087ff292
moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents:
17270
diff
changeset
|
200 |
|
38236
d8c7be27e01d
explicitly distinguish Output.status (essential feedback) vs. Output.report (useful markup);
wenzelm
parents:
36955
diff
changeset
|
201 |
val keyword_statusN = "keyword_status"; |
34243
8821e3293702
report keywords as singleton messages, control message kind via print mode;
wenzelm
parents:
33223
diff
changeset
|
202 |
|
46123 | 203 |
fun status_message m s = |
38413 | 204 |
Position.setmp_thread_data Position.none |
46774 | 205 |
(if print_mode_active keyword_statusN then Output.protocol_message m else writeln) s; |
34243
8821e3293702
report keywords as singleton messages, control message kind via print mode;
wenzelm
parents:
33223
diff
changeset
|
206 |
|
38236
d8c7be27e01d
explicitly distinguish Output.status (essential feedback) vs. Output.report (useful markup);
wenzelm
parents:
36955
diff
changeset
|
207 |
fun keyword_status name = |
46123 | 208 |
status_message (Isabelle_Markup.keyword_decl name) |
209 |
("Outer syntax keyword: " ^ quote name); |
|
27357
5b3a087ff292
moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents:
17270
diff
changeset
|
210 |
|
38236
d8c7be27e01d
explicitly distinguish Output.status (essential feedback) vs. Output.report (useful markup);
wenzelm
parents:
36955
diff
changeset
|
211 |
fun command_status (name, kind) = |
46123 | 212 |
status_message (Isabelle_Markup.command_decl name (kind_of kind)) |
213 |
("Outer syntax command: " ^ quote name ^ " (" ^ kind_of kind ^ ")"); |
|
30670
9bb872667af6
suppress status output for traditional tty modes (including Proof General);
wenzelm
parents:
29347
diff
changeset
|
214 |
|
38236
d8c7be27e01d
explicitly distinguish Output.status (essential feedback) vs. Output.report (useful markup);
wenzelm
parents:
36955
diff
changeset
|
215 |
fun status () = |
46957
0c15caf47040
clarified Keyword.is_keyword: union of minor and major;
wenzelm
parents:
46950
diff
changeset
|
216 |
let |
0c15caf47040
clarified Keyword.is_keyword: union of minor and major;
wenzelm
parents:
46950
diff
changeset
|
217 |
val {lexicons = (minor, _), commands} = get_keywords (); |
0c15caf47040
clarified Keyword.is_keyword: union of minor and major;
wenzelm
parents:
46950
diff
changeset
|
218 |
val _ = List.app keyword_status (sort_strings (Scan.dest_lexicon minor)); |
0c15caf47040
clarified Keyword.is_keyword: union of minor and major;
wenzelm
parents:
46950
diff
changeset
|
219 |
val _ = List.app command_status (sort_wrt #1 (Symtab.dest commands)); |
0c15caf47040
clarified Keyword.is_keyword: union of minor and major;
wenzelm
parents:
46950
diff
changeset
|
220 |
in () end; |
27357
5b3a087ff292
moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents:
17270
diff
changeset
|
221 |
|
5b3a087ff292
moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents:
17270
diff
changeset
|
222 |
|
46958
0ec8f04e753a
define keywords early when processing the theory header, before running the body commands;
wenzelm
parents:
46957
diff
changeset
|
223 |
(* define *) |
27357
5b3a087ff292
moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents:
17270
diff
changeset
|
224 |
|
46958
0ec8f04e753a
define keywords early when processing the theory header, before running the body commands;
wenzelm
parents:
46957
diff
changeset
|
225 |
fun define (name, NONE) = |
46957
0c15caf47040
clarified Keyword.is_keyword: union of minor and major;
wenzelm
parents:
46950
diff
changeset
|
226 |
(change_keywords (fn ((minor, major), commands) => |
0c15caf47040
clarified Keyword.is_keyword: union of minor and major;
wenzelm
parents:
46950
diff
changeset
|
227 |
let |
0c15caf47040
clarified Keyword.is_keyword: union of minor and major;
wenzelm
parents:
46950
diff
changeset
|
228 |
val minor' = Scan.extend_lexicon (Symbol.explode name) minor; |
0c15caf47040
clarified Keyword.is_keyword: union of minor and major;
wenzelm
parents:
46950
diff
changeset
|
229 |
in ((minor', major), commands) end); |
0c15caf47040
clarified Keyword.is_keyword: union of minor and major;
wenzelm
parents:
46950
diff
changeset
|
230 |
keyword_status name) |
46958
0ec8f04e753a
define keywords early when processing the theory header, before running the body commands;
wenzelm
parents:
46957
diff
changeset
|
231 |
| define (name, SOME kind) = |
46957
0c15caf47040
clarified Keyword.is_keyword: union of minor and major;
wenzelm
parents:
46950
diff
changeset
|
232 |
(change_keywords (fn ((minor, major), commands) => |
0c15caf47040
clarified Keyword.is_keyword: union of minor and major;
wenzelm
parents:
46950
diff
changeset
|
233 |
let |
0c15caf47040
clarified Keyword.is_keyword: union of minor and major;
wenzelm
parents:
46950
diff
changeset
|
234 |
val major' = Scan.extend_lexicon (Symbol.explode name) major; |
0c15caf47040
clarified Keyword.is_keyword: union of minor and major;
wenzelm
parents:
46950
diff
changeset
|
235 |
val commands' = Symtab.update (name, kind) commands; |
0c15caf47040
clarified Keyword.is_keyword: union of minor and major;
wenzelm
parents:
46950
diff
changeset
|
236 |
in ((minor, major'), commands') end); |
0c15caf47040
clarified Keyword.is_keyword: union of minor and major;
wenzelm
parents:
46950
diff
changeset
|
237 |
command_status (name, kind)); |
46945 | 238 |
|
27433 | 239 |
|
28431 | 240 |
(* command categories *) |
27433 | 241 |
|
27440
a1eda23752bd
replaced datatype category constructivism by is_theory/is_proof;
wenzelm
parents:
27433
diff
changeset
|
242 |
fun command_category ks name = |
27433 | 243 |
(case command_keyword name of |
27440
a1eda23752bd
replaced datatype category constructivism by is_theory/is_proof;
wenzelm
parents:
27433
diff
changeset
|
244 |
NONE => false |
28431 | 245 |
| SOME k => member (op = o pairself kind_of) ks k); |
27440
a1eda23752bd
replaced datatype category constructivism by is_theory/is_proof;
wenzelm
parents:
27433
diff
changeset
|
246 |
|
29347 | 247 |
val is_diag = command_category [diag]; |
248 |
val is_control = command_category [control]; |
|
40397 | 249 |
val is_regular = not o command_category [diag, control]; |
250 |
||
251 |
val is_heading = command_category [thy_heading, prf_heading]; |
|
29347 | 252 |
|
253 |
val is_theory_begin = command_category [thy_begin]; |
|
254 |
||
27440
a1eda23752bd
replaced datatype category constructivism by is_theory/is_proof;
wenzelm
parents:
27433
diff
changeset
|
255 |
val is_theory = command_category |
36315
e859879079c8
added keyword category "schematic goal", which prevents any attempt to fork the proof;
wenzelm
parents:
34243
diff
changeset
|
256 |
[thy_begin, thy_switch, thy_end, thy_heading, thy_decl, thy_script, thy_goal, thy_schematic_goal]; |
27440
a1eda23752bd
replaced datatype category constructivism by is_theory/is_proof;
wenzelm
parents:
27433
diff
changeset
|
257 |
|
a1eda23752bd
replaced datatype category constructivism by is_theory/is_proof;
wenzelm
parents:
27433
diff
changeset
|
258 |
val is_proof = command_category |
28431 | 259 |
[qed, qed_block, qed_global, prf_heading, prf_goal, prf_block, prf_open, prf_close, |
260 |
prf_chain, prf_decl, prf_asm, prf_asm_goal, prf_script]; |
|
261 |
||
36315
e859879079c8
added keyword category "schematic goal", which prevents any attempt to fork the proof;
wenzelm
parents:
34243
diff
changeset
|
262 |
val is_theory_goal = command_category [thy_goal, thy_schematic_goal]; |
28431 | 263 |
val is_proof_goal = command_category [prf_goal, prf_asm_goal]; |
36315
e859879079c8
added keyword category "schematic goal", which prevents any attempt to fork the proof;
wenzelm
parents:
34243
diff
changeset
|
264 |
val is_schematic_goal = command_category [thy_schematic_goal]; |
28431 | 265 |
val is_qed = command_category [qed, qed_block]; |
266 |
val is_qed_global = command_category [qed_global]; |
|
27520 | 267 |
|
27357
5b3a087ff292
moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents:
17270
diff
changeset
|
268 |
end; |
36949
080e85d46108
renamed structure OuterKeyword to Keyword and OuterParse to Parse, keeping the old names as legacy aliases for some time;
wenzelm
parents:
36681
diff
changeset
|
269 |