author | Fabian Huch <huch@in.tum.de> |
Thu, 18 Jul 2024 13:08:11 +0200 (6 months ago) | |
changeset 80574 | 90493e889dff |
parent 77723 | b761c91c2447 |
child 81628 | e5be995d21f0 |
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 |
|
58900 | 4 |
Isar keyword classification. |
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 |
58928
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58924
diff
changeset
|
9 |
val diag: string |
58999
ed09ae4ea2d8
uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
wenzelm
parents:
58931
diff
changeset
|
10 |
val document_heading: string |
ed09ae4ea2d8
uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
wenzelm
parents:
58931
diff
changeset
|
11 |
val document_body: string |
ed09ae4ea2d8
uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
wenzelm
parents:
58931
diff
changeset
|
12 |
val document_raw: string |
58928
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58924
diff
changeset
|
13 |
val thy_begin: string |
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58924
diff
changeset
|
14 |
val thy_end: string |
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58924
diff
changeset
|
15 |
val thy_decl: string |
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58924
diff
changeset
|
16 |
val thy_decl_block: string |
69913 | 17 |
val thy_defn: string |
18 |
val thy_stmt: string |
|
58928
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58924
diff
changeset
|
19 |
val thy_load: string |
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58924
diff
changeset
|
20 |
val thy_goal: string |
69913 | 21 |
val thy_goal_defn: string |
22 |
val thy_goal_stmt: string |
|
58928
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58924
diff
changeset
|
23 |
val qed: string |
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58924
diff
changeset
|
24 |
val qed_script: string |
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58924
diff
changeset
|
25 |
val qed_block: string |
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58924
diff
changeset
|
26 |
val qed_global: string |
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58924
diff
changeset
|
27 |
val prf_goal: string |
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58924
diff
changeset
|
28 |
val prf_block: string |
60694
b3fa4a8cdb5f
clarified text folds: proof ... qed counts as extra block;
wenzelm
parents:
60693
diff
changeset
|
29 |
val next_block: string |
58928
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58924
diff
changeset
|
30 |
val prf_open: string |
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58924
diff
changeset
|
31 |
val prf_close: string |
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58924
diff
changeset
|
32 |
val prf_chain: string |
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58924
diff
changeset
|
33 |
val prf_decl: string |
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58924
diff
changeset
|
34 |
val prf_asm: string |
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58924
diff
changeset
|
35 |
val prf_asm_goal: string |
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58924
diff
changeset
|
36 |
val prf_script: string |
60624 | 37 |
val prf_script_goal: string |
38 |
val prf_script_asm_goal: string |
|
63441 | 39 |
val before_command: string |
63430 | 40 |
val quasi_command: string |
74671 | 41 |
type spec = {kind: string, load_command: string * Position.T, tags: string list} |
42 |
val command_spec: string * string list -> spec |
|
63429 | 43 |
val no_spec: spec |
63441 | 44 |
val before_command_spec: spec |
63430 | 45 |
val quasi_command_spec: spec |
67139
8fe0aba577af
explicit tag for document commands: avoid implicit use of document_tags;
wenzelm
parents:
63441
diff
changeset
|
46 |
val document_heading_spec: spec |
8fe0aba577af
explicit tag for document commands: avoid implicit use of document_tags;
wenzelm
parents:
63441
diff
changeset
|
47 |
val document_body_spec: spec |
58903 | 48 |
type keywords |
49 |
val minor_keywords: keywords -> Scan.lexicon |
|
50 |
val major_keywords: keywords -> Scan.lexicon |
|
51 |
val empty_keywords: keywords |
|
52 |
val merge_keywords: keywords * keywords -> keywords |
|
63429 | 53 |
val add_keywords: ((string * Position.T) * spec) list -> keywords -> keywords |
74555 | 54 |
val add_minor_keywords: string list -> keywords -> keywords |
74566
8e0f0317e266
ML antiquotations to instantiate types/terms/props;
wenzelm
parents:
74555
diff
changeset
|
55 |
val add_major_keywords: string list -> keywords -> keywords |
74567 | 56 |
val no_major_keywords: keywords -> keywords |
58931 | 57 |
val is_keyword: keywords -> string -> bool |
58 |
val is_command: keywords -> string -> bool |
|
58928
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58924
diff
changeset
|
59 |
val is_literal: keywords -> string -> bool |
61618
27af754f50ca
more thorough check_command, including completion;
wenzelm
parents:
60694
diff
changeset
|
60 |
val dest_commands: keywords -> string list |
59934
b65c4370f831
more position information and PIDE markup for command keywords;
wenzelm
parents:
59735
diff
changeset
|
61 |
val command_markup: keywords -> string -> Markup.T option |
59123
e68e44836d04
imitate command markup and rendering of Isabelle/jEdit in HTML output;
wenzelm
parents:
59033
diff
changeset
|
62 |
val command_kind: keywords -> string -> string option |
58923 | 63 |
val command_tags: keywords -> string -> string list |
58999
ed09ae4ea2d8
uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
wenzelm
parents:
58931
diff
changeset
|
64 |
val is_vacuous: keywords -> string -> bool |
58923 | 65 |
val is_diag: keywords -> string -> bool |
58999
ed09ae4ea2d8
uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
wenzelm
parents:
58931
diff
changeset
|
66 |
val is_document_heading: keywords -> string -> bool |
ed09ae4ea2d8
uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
wenzelm
parents:
58931
diff
changeset
|
67 |
val is_document_body: keywords -> string -> bool |
ed09ae4ea2d8
uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
wenzelm
parents:
58931
diff
changeset
|
68 |
val is_document_raw: keywords -> string -> bool |
59033 | 69 |
val is_document: keywords -> string -> bool |
59125 | 70 |
val is_theory_end: keywords -> string -> bool |
58923 | 71 |
val is_theory_load: keywords -> string -> bool |
72 |
val is_theory: keywords -> string -> bool |
|
73 |
val is_theory_body: keywords -> string -> bool |
|
74 |
val is_proof: keywords -> string -> bool |
|
75 |
val is_proof_body: keywords -> string -> bool |
|
76 |
val is_theory_goal: keywords -> string -> bool |
|
77 |
val is_proof_goal: keywords -> string -> bool |
|
78 |
val is_qed: keywords -> string -> bool |
|
79 |
val is_qed_global: keywords -> string -> bool |
|
60693
044f8bb3dd30
more accurate skip_proofs nesting, e.g. relevant for 'subgoal' command;
wenzelm
parents:
60624
diff
changeset
|
80 |
val is_proof_open: keywords -> string -> bool |
044f8bb3dd30
more accurate skip_proofs nesting, e.g. relevant for 'subgoal' command;
wenzelm
parents:
60624
diff
changeset
|
81 |
val is_proof_close: keywords -> string -> bool |
59125 | 82 |
val is_proof_asm: keywords -> string -> bool |
83 |
val is_improper: keywords -> string -> bool |
|
58923 | 84 |
val is_printed: keywords -> string -> bool |
17059
a001a3ebfcfd
Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff
changeset
|
85 |
end; |
a001a3ebfcfd
Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff
changeset
|
86 |
|
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
|
87 |
structure Keyword: KEYWORD = |
17059
a001a3ebfcfd
Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff
changeset
|
88 |
struct |
a001a3ebfcfd
Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff
changeset
|
89 |
|
27357
5b3a087ff292
moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents:
17270
diff
changeset
|
90 |
(** keyword classification **) |
17059
a001a3ebfcfd
Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff
changeset
|
91 |
|
58918 | 92 |
(* kinds *) |
93 |
||
58928
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58924
diff
changeset
|
94 |
val diag = "diag"; |
58999
ed09ae4ea2d8
uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
wenzelm
parents:
58931
diff
changeset
|
95 |
val document_heading = "document_heading"; |
ed09ae4ea2d8
uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
wenzelm
parents:
58931
diff
changeset
|
96 |
val document_body = "document_body"; |
ed09ae4ea2d8
uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
wenzelm
parents:
58931
diff
changeset
|
97 |
val document_raw = "document_raw"; |
58928
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58924
diff
changeset
|
98 |
val thy_begin = "thy_begin"; |
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58924
diff
changeset
|
99 |
val thy_end = "thy_end"; |
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58924
diff
changeset
|
100 |
val thy_decl = "thy_decl"; |
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58924
diff
changeset
|
101 |
val thy_decl_block = "thy_decl_block"; |
69913 | 102 |
val thy_defn = "thy_defn"; |
103 |
val thy_stmt = "thy_stmt"; |
|
58928
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58924
diff
changeset
|
104 |
val thy_load = "thy_load"; |
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58924
diff
changeset
|
105 |
val thy_goal = "thy_goal"; |
69913 | 106 |
val thy_goal_defn = "thy_goal_defn"; |
107 |
val thy_goal_stmt = "thy_goal_stmt"; |
|
58928
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58924
diff
changeset
|
108 |
val qed = "qed"; |
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58924
diff
changeset
|
109 |
val qed_script = "qed_script"; |
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58924
diff
changeset
|
110 |
val qed_block = "qed_block"; |
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58924
diff
changeset
|
111 |
val qed_global = "qed_global"; |
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58924
diff
changeset
|
112 |
val prf_goal = "prf_goal"; |
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58924
diff
changeset
|
113 |
val prf_block = "prf_block"; |
60694
b3fa4a8cdb5f
clarified text folds: proof ... qed counts as extra block;
wenzelm
parents:
60693
diff
changeset
|
114 |
val next_block = "next_block"; |
58928
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58924
diff
changeset
|
115 |
val prf_open = "prf_open"; |
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58924
diff
changeset
|
116 |
val prf_close = "prf_close"; |
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58924
diff
changeset
|
117 |
val prf_chain = "prf_chain"; |
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58924
diff
changeset
|
118 |
val prf_decl = "prf_decl"; |
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58924
diff
changeset
|
119 |
val prf_asm = "prf_asm"; |
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58924
diff
changeset
|
120 |
val prf_asm_goal = "prf_asm_goal"; |
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58924
diff
changeset
|
121 |
val prf_script = "prf_script"; |
60624 | 122 |
val prf_script_goal = "prf_script_goal"; |
123 |
val prf_script_asm_goal = "prf_script_asm_goal"; |
|
63441 | 124 |
|
125 |
val before_command = "before_command"; |
|
63430 | 126 |
val quasi_command = "quasi_command"; |
58928
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58924
diff
changeset
|
127 |
|
63430 | 128 |
val command_kinds = |
58999
ed09ae4ea2d8
uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
wenzelm
parents:
58931
diff
changeset
|
129 |
[diag, document_heading, document_body, document_raw, thy_begin, thy_end, thy_load, thy_decl, |
69913 | 130 |
thy_decl_block, thy_defn, thy_stmt, thy_goal, thy_goal_defn, thy_goal_stmt, qed, qed_script, |
131 |
qed_block, qed_global, prf_goal, prf_block, next_block, prf_open, prf_close, prf_chain, |
|
132 |
prf_decl, prf_asm, prf_asm_goal, prf_script, prf_script_goal, prf_script_asm_goal]; |
|
58928
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58924
diff
changeset
|
133 |
|
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58924
diff
changeset
|
134 |
|
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58924
diff
changeset
|
135 |
(* specifications *) |
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58924
diff
changeset
|
136 |
|
74671 | 137 |
type spec = {kind: string, load_command: string * Position.T, tags: string list}; |
138 |
||
139 |
fun command_spec (kind, tags) : spec = |
|
140 |
{kind = kind, load_command = ("", Position.none), tags = tags}; |
|
59934
b65c4370f831
more position information and PIDE markup for command keywords;
wenzelm
parents:
59735
diff
changeset
|
141 |
|
74671 | 142 |
val no_spec = command_spec ("", []); |
143 |
val before_command_spec = command_spec (before_command, []); |
|
144 |
val quasi_command_spec = command_spec (quasi_command, []); |
|
145 |
val document_heading_spec = command_spec ("document_heading", ["document"]); |
|
146 |
val document_body_spec = command_spec ("document_body", ["document"]); |
|
63429 | 147 |
|
59934
b65c4370f831
more position information and PIDE markup for command keywords;
wenzelm
parents:
59735
diff
changeset
|
148 |
type entry = |
b65c4370f831
more position information and PIDE markup for command keywords;
wenzelm
parents:
59735
diff
changeset
|
149 |
{pos: Position.T, |
b65c4370f831
more position information and PIDE markup for command keywords;
wenzelm
parents:
59735
diff
changeset
|
150 |
id: serial, |
b65c4370f831
more position information and PIDE markup for command keywords;
wenzelm
parents:
59735
diff
changeset
|
151 |
kind: string, |
58918 | 152 |
tags: string list}; |
17059
a001a3ebfcfd
Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff
changeset
|
153 |
|
74671 | 154 |
fun check_spec pos ({kind, tags, ...}: spec) : entry = |
63430 | 155 |
if not (member (op =) command_kinds kind) then |
58918 | 156 |
error ("Unknown outer syntax keyword kind " ^ quote kind) |
72747
5f9d66155081
clarified theory keywords: loaded_files are determined statically in Scala, but ML needs to do it semantically;
wenzelm
parents:
69913
diff
changeset
|
157 |
else {pos = pos, id = serial (), kind = kind, tags = tags}; |
46961
5c6955f487e5
outer syntax command definitions based on formal command_spec derived from theory header declarations;
wenzelm
parents:
46958
diff
changeset
|
158 |
|
46938
cda018294515
some support for outer syntax keyword declarations within theory header;
wenzelm
parents:
46924
diff
changeset
|
159 |
|
58903 | 160 |
(** keyword tables **) |
161 |
||
162 |
(* type keywords *) |
|
27357
5b3a087ff292
moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents:
17270
diff
changeset
|
163 |
|
48874
ff9cd47be39b
refined Thy_Load.check_thy: find more uses in body text, based on keywords;
wenzelm
parents:
48872
diff
changeset
|
164 |
datatype keywords = Keywords of |
58903 | 165 |
{minor: Scan.lexicon, |
166 |
major: Scan.lexicon, |
|
59934
b65c4370f831
more position information and PIDE markup for command keywords;
wenzelm
parents:
59735
diff
changeset
|
167 |
commands: entry Symtab.table}; |
58903 | 168 |
|
169 |
fun minor_keywords (Keywords {minor, ...}) = minor; |
|
170 |
fun major_keywords (Keywords {major, ...}) = major; |
|
171 |
||
58906 | 172 |
fun make_keywords (minor, major, commands) = |
173 |
Keywords {minor = minor, major = major, commands = commands}; |
|
46957
0c15caf47040
clarified Keyword.is_keyword: union of minor and major;
wenzelm
parents:
46950
diff
changeset
|
174 |
|
58906 | 175 |
fun map_keywords f (Keywords {minor, major, commands}) = |
176 |
make_keywords (f (minor, major, commands)); |
|
58903 | 177 |
|
58920 | 178 |
|
179 |
(* build keywords *) |
|
180 |
||
58903 | 181 |
val empty_keywords = |
182 |
make_keywords (Scan.empty_lexicon, Scan.empty_lexicon, Symtab.empty); |
|
48874
ff9cd47be39b
refined Thy_Load.check_thy: find more uses in body text, based on keywords;
wenzelm
parents:
48872
diff
changeset
|
183 |
|
58903 | 184 |
fun merge_keywords |
58906 | 185 |
(Keywords {minor = minor1, major = major1, commands = commands1}, |
186 |
Keywords {minor = minor2, major = major2, commands = commands2}) = |
|
58903 | 187 |
make_keywords |
188 |
(Scan.merge_lexicons (minor1, minor2), |
|
189 |
Scan.merge_lexicons (major1, major2), |
|
58906 | 190 |
Symtab.merge (K true) (commands1, commands2)); |
27357
5b3a087ff292
moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents:
17270
diff
changeset
|
191 |
|
58928
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58924
diff
changeset
|
192 |
val add_keywords = |
74671 | 193 |
fold (fn ((name, pos), spec as {kind, ...}: spec) => map_keywords (fn (minor, major, commands) => |
63441 | 194 |
if kind = "" orelse kind = before_command orelse kind = quasi_command then |
63429 | 195 |
let |
196 |
val minor' = Scan.extend_lexicon (Symbol.explode name) minor; |
|
197 |
in (minor', major, commands) end |
|
198 |
else |
|
199 |
let |
|
200 |
val entry = check_spec pos spec; |
|
201 |
val major' = Scan.extend_lexicon (Symbol.explode name) major; |
|
202 |
val commands' = Symtab.update (name, entry) commands; |
|
203 |
in (minor, major', commands') end)); |
|
27357
5b3a087ff292
moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents:
17270
diff
changeset
|
204 |
|
74555 | 205 |
val add_minor_keywords = |
206 |
add_keywords o map (fn name => ((name, Position.none), no_spec)); |
|
207 |
||
74566
8e0f0317e266
ML antiquotations to instantiate types/terms/props;
wenzelm
parents:
74555
diff
changeset
|
208 |
val add_major_keywords = |
74671 | 209 |
add_keywords o map (fn name => ((name, Position.none), command_spec (diag, []))); |
74566
8e0f0317e266
ML antiquotations to instantiate types/terms/props;
wenzelm
parents:
74555
diff
changeset
|
210 |
|
74567 | 211 |
val no_major_keywords = |
212 |
map_keywords (fn (minor, _, _) => (minor, Scan.empty_lexicon, Symtab.empty)); |
|
213 |
||
58903 | 214 |
|
58931 | 215 |
(* keyword status *) |
27357
5b3a087ff292
moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents:
17270
diff
changeset
|
216 |
|
58931 | 217 |
fun is_keyword keywords s = Scan.is_literal (minor_keywords keywords) (Symbol.explode s); |
218 |
fun is_command (Keywords {commands, ...}) = Symtab.defined commands; |
|
219 |
fun is_literal keywords = is_keyword keywords orf is_command keywords; |
|
27357
5b3a087ff292
moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents:
17270
diff
changeset
|
220 |
|
61618
27af754f50ca
more thorough check_command, including completion;
wenzelm
parents:
60694
diff
changeset
|
221 |
fun dest_commands (Keywords {commands, ...}) = Symtab.keys commands; |
27af754f50ca
more thorough check_command, including completion;
wenzelm
parents:
60694
diff
changeset
|
222 |
|
58928
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58924
diff
changeset
|
223 |
|
59934
b65c4370f831
more position information and PIDE markup for command keywords;
wenzelm
parents:
59735
diff
changeset
|
224 |
(* command keywords *) |
58931 | 225 |
|
59123
e68e44836d04
imitate command markup and rendering of Isabelle/jEdit in HTML output;
wenzelm
parents:
59033
diff
changeset
|
226 |
fun lookup_command (Keywords {commands, ...}) = Symtab.lookup commands; |
e68e44836d04
imitate command markup and rendering of Isabelle/jEdit in HTML output;
wenzelm
parents:
59033
diff
changeset
|
227 |
|
59934
b65c4370f831
more position information and PIDE markup for command keywords;
wenzelm
parents:
59735
diff
changeset
|
228 |
fun command_markup keywords name = |
b65c4370f831
more position information and PIDE markup for command keywords;
wenzelm
parents:
59735
diff
changeset
|
229 |
lookup_command keywords name |
b65c4370f831
more position information and PIDE markup for command keywords;
wenzelm
parents:
59735
diff
changeset
|
230 |
|> Option.map (fn {pos, id, ...} => |
74262 | 231 |
Position.make_entity_markup {def = false} id Markup.command_keywordN (name, pos)); |
59934
b65c4370f831
more position information and PIDE markup for command keywords;
wenzelm
parents:
59735
diff
changeset
|
232 |
|
59123
e68e44836d04
imitate command markup and rendering of Isabelle/jEdit in HTML output;
wenzelm
parents:
59033
diff
changeset
|
233 |
fun command_kind keywords = Option.map #kind o lookup_command keywords; |
54523 | 234 |
|
58923 | 235 |
fun command_tags keywords name = |
59123
e68e44836d04
imitate command markup and rendering of Isabelle/jEdit in HTML output;
wenzelm
parents:
59033
diff
changeset
|
236 |
(case lookup_command keywords name of |
58928
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58924
diff
changeset
|
237 |
SOME {tags, ...} => tags |
58918 | 238 |
| NONE => []); |
27357
5b3a087ff292
moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents:
17270
diff
changeset
|
239 |
|
27433 | 240 |
|
28431 | 241 |
(* command categories *) |
27433 | 242 |
|
51225 | 243 |
fun command_category ks = |
58923 | 244 |
let |
77723
b761c91c2447
performance tuning: prefer functor Set() over Table();
wenzelm
parents:
74671
diff
changeset
|
245 |
val set = Symset.make ks; |
58923 | 246 |
fun pred keywords name = |
59123
e68e44836d04
imitate command markup and rendering of Isabelle/jEdit in HTML output;
wenzelm
parents:
59033
diff
changeset
|
247 |
(case lookup_command keywords name of |
51225 | 248 |
NONE => false |
77723
b761c91c2447
performance tuning: prefer functor Set() over Table();
wenzelm
parents:
74671
diff
changeset
|
249 |
| SOME {kind, ...} => Symset.member set kind); |
58923 | 250 |
in pred end; |
27440
a1eda23752bd
replaced datatype category constructivism by is_theory/is_proof;
wenzelm
parents:
27433
diff
changeset
|
251 |
|
58999
ed09ae4ea2d8
uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
wenzelm
parents:
58931
diff
changeset
|
252 |
val is_vacuous = command_category [diag, document_heading, document_body, document_raw]; |
ed09ae4ea2d8
uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
wenzelm
parents:
58931
diff
changeset
|
253 |
|
29347 | 254 |
val is_diag = command_category [diag]; |
40397 | 255 |
|
58999
ed09ae4ea2d8
uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
wenzelm
parents:
58931
diff
changeset
|
256 |
val is_document_heading = command_category [document_heading]; |
ed09ae4ea2d8
uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
wenzelm
parents:
58931
diff
changeset
|
257 |
val is_document_body = command_category [document_body]; |
ed09ae4ea2d8
uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
wenzelm
parents:
58931
diff
changeset
|
258 |
val is_document_raw = command_category [document_raw]; |
ed09ae4ea2d8
uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
wenzelm
parents:
58931
diff
changeset
|
259 |
val is_document = command_category [document_heading, document_body, document_raw]; |
29347 | 260 |
|
59125 | 261 |
val is_theory_end = command_category [thy_end]; |
29347 | 262 |
|
48867
e9beabf045ab
some support for inlining file content into outer syntax token language;
wenzelm
parents:
48864
diff
changeset
|
263 |
val is_theory_load = command_category [thy_load]; |
e9beabf045ab
some support for inlining file content into outer syntax token language;
wenzelm
parents:
48864
diff
changeset
|
264 |
|
27440
a1eda23752bd
replaced datatype category constructivism by is_theory/is_proof;
wenzelm
parents:
27433
diff
changeset
|
265 |
val is_theory = command_category |
69913 | 266 |
[thy_begin, thy_end, thy_load, thy_decl, thy_decl_block, thy_defn, thy_stmt, thy_goal, |
267 |
thy_goal_defn, thy_goal_stmt]; |
|
27440
a1eda23752bd
replaced datatype category constructivism by is_theory/is_proof;
wenzelm
parents:
27433
diff
changeset
|
268 |
|
56944
578dc6b4be89
no reset for 'end' -- e.g. relevant for 'notepad';
wenzelm
parents:
56895
diff
changeset
|
269 |
val is_theory_body = command_category |
69913 | 270 |
[thy_load, thy_decl, thy_decl_block, thy_defn, thy_stmt, thy_goal, thy_goal_defn, thy_goal_stmt]; |
56944
578dc6b4be89
no reset for 'end' -- e.g. relevant for 'notepad';
wenzelm
parents:
56895
diff
changeset
|
271 |
|
27440
a1eda23752bd
replaced datatype category constructivism by is_theory/is_proof;
wenzelm
parents:
27433
diff
changeset
|
272 |
val is_proof = command_category |
60694
b3fa4a8cdb5f
clarified text folds: proof ... qed counts as extra block;
wenzelm
parents:
60693
diff
changeset
|
273 |
[qed, qed_script, qed_block, qed_global, prf_goal, prf_block, next_block, prf_open, |
b3fa4a8cdb5f
clarified text folds: proof ... qed counts as extra block;
wenzelm
parents:
60693
diff
changeset
|
274 |
prf_close, prf_chain, prf_decl, prf_asm, prf_asm_goal, prf_script, prf_script_goal, |
60624 | 275 |
prf_script_asm_goal]; |
28431 | 276 |
|
51225 | 277 |
val is_proof_body = command_category |
60694
b3fa4a8cdb5f
clarified text folds: proof ... qed counts as extra block;
wenzelm
parents:
60693
diff
changeset
|
278 |
[diag, document_heading, document_body, document_raw, prf_block, next_block, prf_open, |
b3fa4a8cdb5f
clarified text folds: proof ... qed counts as extra block;
wenzelm
parents:
60693
diff
changeset
|
279 |
prf_close, prf_chain, prf_decl, prf_asm, prf_asm_goal, prf_script, prf_script_goal, |
60624 | 280 |
prf_script_asm_goal]; |
51225 | 281 |
|
69913 | 282 |
val is_theory_goal = command_category [thy_goal, thy_goal_defn, thy_goal_stmt]; |
60624 | 283 |
val is_proof_goal = command_category [prf_goal, prf_asm_goal, prf_script_goal, prf_script_asm_goal]; |
53571
e58ca0311c0f
more explicit indication of 'done' as proof script element;
wenzelm
parents:
53371
diff
changeset
|
284 |
val is_qed = command_category [qed, qed_script, qed_block]; |
28431 | 285 |
val is_qed_global = command_category [qed_global]; |
27520 | 286 |
|
60693
044f8bb3dd30
more accurate skip_proofs nesting, e.g. relevant for 'subgoal' command;
wenzelm
parents:
60624
diff
changeset
|
287 |
val is_proof_open = |
044f8bb3dd30
more accurate skip_proofs nesting, e.g. relevant for 'subgoal' command;
wenzelm
parents:
60624
diff
changeset
|
288 |
command_category [prf_goal, prf_asm_goal, prf_script_goal, prf_script_asm_goal, prf_open]; |
044f8bb3dd30
more accurate skip_proofs nesting, e.g. relevant for 'subgoal' command;
wenzelm
parents:
60624
diff
changeset
|
289 |
val is_proof_close = command_category [qed, qed_script, qed_block, prf_close]; |
044f8bb3dd30
more accurate skip_proofs nesting, e.g. relevant for 'subgoal' command;
wenzelm
parents:
60624
diff
changeset
|
290 |
|
59125 | 291 |
val is_proof_asm = command_category [prf_asm, prf_asm_goal]; |
60624 | 292 |
val is_improper = command_category [qed_script, prf_script, prf_script_goal, prf_script_asm_goal]; |
59125 | 293 |
|
58923 | 294 |
fun is_printed keywords = is_theory_goal keywords orf is_proof keywords; |
295 |
||
27357
5b3a087ff292
moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents:
17270
diff
changeset
|
296 |
end; |