author | wenzelm |
Wed, 05 Nov 2014 21:21:15 +0100 | |
changeset 58906 | 29788e989d61 |
parent 58903 | 38c72f5f6c2e |
child 58918 | 8d36bc5eaed3 |
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 |
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 |
48864
3ee314ae1e0a
added keyword kind "thy_load" (with optional list of file extensions);
wenzelm
parents:
48709
diff
changeset
|
11 |
val kind_files_of: T -> string * string list |
17059
a001a3ebfcfd
Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff
changeset
|
12 |
val diag: T |
58868
c5e1cce7ace3
uniform heading commands work in any context, even in theory header;
wenzelm
parents:
58853
diff
changeset
|
13 |
val heading: T |
17059
a001a3ebfcfd
Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff
changeset
|
14 |
val thy_begin: 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_decl: T |
58800
bfed1c26caed
explicit keyword category for commands that may start a block;
wenzelm
parents:
56944
diff
changeset
|
17 |
val thy_decl_block: T |
48864
3ee314ae1e0a
added keyword kind "thy_load" (with optional list of file extensions);
wenzelm
parents:
48709
diff
changeset
|
18 |
val thy_load: T |
3ee314ae1e0a
added keyword kind "thy_load" (with optional list of file extensions);
wenzelm
parents:
48709
diff
changeset
|
19 |
val thy_load_files: string list -> T |
17059
a001a3ebfcfd
Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff
changeset
|
20 |
val thy_goal: T |
a001a3ebfcfd
Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff
changeset
|
21 |
val qed: T |
53571
e58ca0311c0f
more explicit indication of 'done' as proof script element;
wenzelm
parents:
53371
diff
changeset
|
22 |
val qed_script: T |
17059
a001a3ebfcfd
Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff
changeset
|
23 |
val qed_block: T |
a001a3ebfcfd
Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff
changeset
|
24 |
val qed_global: 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 |
53371
47b23c582127
more explicit indication of 'guess' as improper Isar (aka "script") element;
wenzelm
parents:
52440
diff
changeset
|
33 |
val prf_asm_goal_script: T |
17059
a001a3ebfcfd
Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff
changeset
|
34 |
val prf_script: T |
46968 | 35 |
val kinds: T list |
17059
a001a3ebfcfd
Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff
changeset
|
36 |
val tag: string -> T -> T |
a001a3ebfcfd
Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff
changeset
|
37 |
val tags_of: T -> string list |
a001a3ebfcfd
Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff
changeset
|
38 |
val tag_theory: T -> T |
a001a3ebfcfd
Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff
changeset
|
39 |
val tag_proof: T -> T |
a001a3ebfcfd
Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff
changeset
|
40 |
val tag_ml: T -> T |
48864
3ee314ae1e0a
added keyword kind "thy_load" (with optional list of file extensions);
wenzelm
parents:
48709
diff
changeset
|
41 |
type spec = (string * string list) * string list |
46961
5c6955f487e5
outer syntax command definitions based on formal command_spec derived from theory header declarations;
wenzelm
parents:
46958
diff
changeset
|
42 |
val spec: spec -> T |
48646
91281e9472d8
more official command specifications, including source position;
wenzelm
parents:
46969
diff
changeset
|
43 |
val command_spec: (string * spec) * Position.T -> (string * T) * Position.T |
58903 | 44 |
type keywords |
45 |
val minor_keywords: keywords -> Scan.lexicon |
|
46 |
val major_keywords: keywords -> Scan.lexicon |
|
47 |
val empty_keywords: keywords |
|
48 |
val merge_keywords: keywords * keywords -> keywords |
|
49 |
val no_command_keywords: keywords -> keywords |
|
50 |
val add: string * T option -> keywords -> keywords |
|
51 |
val define: string * T option -> unit |
|
52 |
val get_keywords: unit -> keywords |
|
27357
5b3a087ff292
moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents:
17270
diff
changeset
|
53 |
val get_lexicons: unit -> Scan.lexicon * Scan.lexicon |
5b3a087ff292
moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents:
17270
diff
changeset
|
54 |
val is_keyword: string -> bool |
5b3a087ff292
moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents:
17270
diff
changeset
|
55 |
val command_keyword: string -> T option |
54523 | 56 |
val command_files: string -> Path.T -> Path.T list |
27357
5b3a087ff292
moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents:
17270
diff
changeset
|
57 |
val command_tags: string -> string list |
29347 | 58 |
val is_diag: string -> bool |
40397 | 59 |
val is_heading: string -> bool |
29347 | 60 |
val is_theory_begin: string -> bool |
48867
e9beabf045ab
some support for inlining file content into outer syntax token language;
wenzelm
parents:
48864
diff
changeset
|
61 |
val is_theory_load: string -> bool |
27440
a1eda23752bd
replaced datatype category constructivism by is_theory/is_proof;
wenzelm
parents:
27433
diff
changeset
|
62 |
val is_theory: string -> bool |
56944
578dc6b4be89
no reset for 'end' -- e.g. relevant for 'notepad';
wenzelm
parents:
56895
diff
changeset
|
63 |
val is_theory_body: string -> bool |
27440
a1eda23752bd
replaced datatype category constructivism by is_theory/is_proof;
wenzelm
parents:
27433
diff
changeset
|
64 |
val is_proof: string -> bool |
51225 | 65 |
val is_proof_body: string -> bool |
28431 | 66 |
val is_theory_goal: string -> bool |
67 |
val is_proof_goal: string -> bool |
|
68 |
val is_qed: string -> bool |
|
69 |
val is_qed_global: string -> bool |
|
56895
f058120aaad4
discontinued Toplevel.print flag -- print uniformly according to Keyword.is_printed;
wenzelm
parents:
56146
diff
changeset
|
70 |
val is_printed: string -> bool |
17059
a001a3ebfcfd
Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff
changeset
|
71 |
end; |
a001a3ebfcfd
Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff
changeset
|
72 |
|
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
|
73 |
structure Keyword: KEYWORD = |
17059
a001a3ebfcfd
Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff
changeset
|
74 |
struct |
a001a3ebfcfd
Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff
changeset
|
75 |
|
27357
5b3a087ff292
moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents:
17270
diff
changeset
|
76 |
(** keyword classification **) |
17059
a001a3ebfcfd
Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff
changeset
|
77 |
|
48864
3ee314ae1e0a
added keyword kind "thy_load" (with optional list of file extensions);
wenzelm
parents:
48709
diff
changeset
|
78 |
datatype T = Keyword of |
3ee314ae1e0a
added keyword kind "thy_load" (with optional list of file extensions);
wenzelm
parents:
48709
diff
changeset
|
79 |
{kind: string, |
3ee314ae1e0a
added keyword kind "thy_load" (with optional list of file extensions);
wenzelm
parents:
48709
diff
changeset
|
80 |
files: string list, (*extensions of embedded files*) |
3ee314ae1e0a
added keyword kind "thy_load" (with optional list of file extensions);
wenzelm
parents:
48709
diff
changeset
|
81 |
tags: string list}; (*tags in canonical reverse order*) |
17059
a001a3ebfcfd
Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff
changeset
|
82 |
|
48864
3ee314ae1e0a
added keyword kind "thy_load" (with optional list of file extensions);
wenzelm
parents:
48709
diff
changeset
|
83 |
fun kind s = Keyword {kind = s, files = [], tags = []}; |
3ee314ae1e0a
added keyword kind "thy_load" (with optional list of file extensions);
wenzelm
parents:
48709
diff
changeset
|
84 |
fun kind_of (Keyword {kind, ...}) = kind; |
3ee314ae1e0a
added keyword kind "thy_load" (with optional list of file extensions);
wenzelm
parents:
48709
diff
changeset
|
85 |
fun kind_files_of (Keyword {kind, files, ...}) = (kind, files); |
3ee314ae1e0a
added keyword kind "thy_load" (with optional list of file extensions);
wenzelm
parents:
48709
diff
changeset
|
86 |
|
3ee314ae1e0a
added keyword kind "thy_load" (with optional list of file extensions);
wenzelm
parents:
48709
diff
changeset
|
87 |
fun add_files fs (Keyword {kind, files, tags}) = |
3ee314ae1e0a
added keyword kind "thy_load" (with optional list of file extensions);
wenzelm
parents:
48709
diff
changeset
|
88 |
Keyword {kind = kind, files = files @ fs, tags = tags}; |
17059
a001a3ebfcfd
Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff
changeset
|
89 |
|
a001a3ebfcfd
Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff
changeset
|
90 |
|
a001a3ebfcfd
Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff
changeset
|
91 |
(* kinds *) |
a001a3ebfcfd
Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff
changeset
|
92 |
|
a001a3ebfcfd
Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff
changeset
|
93 |
val diag = kind "diag"; |
58868
c5e1cce7ace3
uniform heading commands work in any context, even in theory header;
wenzelm
parents:
58853
diff
changeset
|
94 |
val heading = kind "heading"; |
46967
499d9bbd8de9
uniform keyword names within ML/Scala -- produce elisp names via external conversion;
wenzelm
parents:
46961
diff
changeset
|
95 |
val thy_begin = kind "thy_begin"; |
499d9bbd8de9
uniform keyword names within ML/Scala -- produce elisp names via external conversion;
wenzelm
parents:
46961
diff
changeset
|
96 |
val thy_end = kind "thy_end"; |
48867
e9beabf045ab
some support for inlining file content into outer syntax token language;
wenzelm
parents:
48864
diff
changeset
|
97 |
val thy_decl = kind "thy_decl"; |
58800
bfed1c26caed
explicit keyword category for commands that may start a block;
wenzelm
parents:
56944
diff
changeset
|
98 |
val thy_decl_block = kind "thy_decl_block"; |
48864
3ee314ae1e0a
added keyword kind "thy_load" (with optional list of file extensions);
wenzelm
parents:
48709
diff
changeset
|
99 |
val thy_load = kind "thy_load"; |
3ee314ae1e0a
added keyword kind "thy_load" (with optional list of file extensions);
wenzelm
parents:
48709
diff
changeset
|
100 |
fun thy_load_files files = Keyword {kind = "thy_load", files = files, tags = []}; |
46967
499d9bbd8de9
uniform keyword names within ML/Scala -- produce elisp names via external conversion;
wenzelm
parents:
46961
diff
changeset
|
101 |
val thy_goal = kind "thy_goal"; |
17059
a001a3ebfcfd
Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff
changeset
|
102 |
val qed = kind "qed"; |
53571
e58ca0311c0f
more explicit indication of 'done' as proof script element;
wenzelm
parents:
53371
diff
changeset
|
103 |
val qed_script = kind "qed_script"; |
46967
499d9bbd8de9
uniform keyword names within ML/Scala -- produce elisp names via external conversion;
wenzelm
parents:
46961
diff
changeset
|
104 |
val qed_block = kind "qed_block"; |
499d9bbd8de9
uniform keyword names within ML/Scala -- produce elisp names via external conversion;
wenzelm
parents:
46961
diff
changeset
|
105 |
val qed_global = kind "qed_global"; |
499d9bbd8de9
uniform keyword names within ML/Scala -- produce elisp names via external conversion;
wenzelm
parents:
46961
diff
changeset
|
106 |
val prf_goal = kind "prf_goal"; |
499d9bbd8de9
uniform keyword names within ML/Scala -- produce elisp names via external conversion;
wenzelm
parents:
46961
diff
changeset
|
107 |
val prf_block = kind "prf_block"; |
499d9bbd8de9
uniform keyword names within ML/Scala -- produce elisp names via external conversion;
wenzelm
parents:
46961
diff
changeset
|
108 |
val prf_open = kind "prf_open"; |
499d9bbd8de9
uniform keyword names within ML/Scala -- produce elisp names via external conversion;
wenzelm
parents:
46961
diff
changeset
|
109 |
val prf_close = kind "prf_close"; |
499d9bbd8de9
uniform keyword names within ML/Scala -- produce elisp names via external conversion;
wenzelm
parents:
46961
diff
changeset
|
110 |
val prf_chain = kind "prf_chain"; |
499d9bbd8de9
uniform keyword names within ML/Scala -- produce elisp names via external conversion;
wenzelm
parents:
46961
diff
changeset
|
111 |
val prf_decl = kind "prf_decl"; |
499d9bbd8de9
uniform keyword names within ML/Scala -- produce elisp names via external conversion;
wenzelm
parents:
46961
diff
changeset
|
112 |
val prf_asm = kind "prf_asm"; |
499d9bbd8de9
uniform keyword names within ML/Scala -- produce elisp names via external conversion;
wenzelm
parents:
46961
diff
changeset
|
113 |
val prf_asm_goal = kind "prf_asm_goal"; |
53371
47b23c582127
more explicit indication of 'guess' as improper Isar (aka "script") element;
wenzelm
parents:
52440
diff
changeset
|
114 |
val prf_asm_goal_script = kind "prf_asm_goal_script"; |
46967
499d9bbd8de9
uniform keyword names within ML/Scala -- produce elisp names via external conversion;
wenzelm
parents:
46961
diff
changeset
|
115 |
val prf_script = kind "prf_script"; |
17059
a001a3ebfcfd
Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff
changeset
|
116 |
|
36315
e859879079c8
added keyword category "schematic goal", which prevents any attempt to fork the proof;
wenzelm
parents:
34243
diff
changeset
|
117 |
val kinds = |
58868
c5e1cce7ace3
uniform heading commands work in any context, even in theory header;
wenzelm
parents:
58853
diff
changeset
|
118 |
[diag, heading, thy_begin, thy_end, thy_load, thy_decl, thy_decl_block, thy_goal, |
c5e1cce7ace3
uniform heading commands work in any context, even in theory header;
wenzelm
parents:
58853
diff
changeset
|
119 |
qed, qed_script, qed_block, qed_global, prf_goal, prf_block, prf_open, prf_close, |
c5e1cce7ace3
uniform heading commands work in any context, even in theory header;
wenzelm
parents:
58853
diff
changeset
|
120 |
prf_chain, prf_decl, prf_asm, prf_asm_goal, prf_asm_goal_script, prf_script]; |
17059
a001a3ebfcfd
Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff
changeset
|
121 |
|
a001a3ebfcfd
Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff
changeset
|
122 |
|
a001a3ebfcfd
Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff
changeset
|
123 |
(* tags *) |
a001a3ebfcfd
Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff
changeset
|
124 |
|
48864
3ee314ae1e0a
added keyword kind "thy_load" (with optional list of file extensions);
wenzelm
parents:
48709
diff
changeset
|
125 |
fun tag t (Keyword {kind, files, tags}) = |
3ee314ae1e0a
added keyword kind "thy_load" (with optional list of file extensions);
wenzelm
parents:
48709
diff
changeset
|
126 |
Keyword {kind = kind, files = files, tags = update (op =) t tags}; |
3ee314ae1e0a
added keyword kind "thy_load" (with optional list of file extensions);
wenzelm
parents:
48709
diff
changeset
|
127 |
fun tags_of (Keyword {tags, ...}) = tags; |
17059
a001a3ebfcfd
Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff
changeset
|
128 |
|
a001a3ebfcfd
Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff
changeset
|
129 |
val tag_theory = tag "theory"; |
a001a3ebfcfd
Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff
changeset
|
130 |
val tag_proof = tag "proof"; |
a001a3ebfcfd
Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff
changeset
|
131 |
val tag_ml = tag "ML"; |
a001a3ebfcfd
Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff
changeset
|
132 |
|
27357
5b3a087ff292
moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents:
17270
diff
changeset
|
133 |
|
46938
cda018294515
some support for outer syntax keyword declarations within theory header;
wenzelm
parents:
46924
diff
changeset
|
134 |
(* external names *) |
cda018294515
some support for outer syntax keyword declarations within theory header;
wenzelm
parents:
46924
diff
changeset
|
135 |
|
46968 | 136 |
val name_table = Symtab.make (map (`kind_of) kinds); |
46938
cda018294515
some support for outer syntax keyword declarations within theory header;
wenzelm
parents:
46924
diff
changeset
|
137 |
|
48864
3ee314ae1e0a
added keyword kind "thy_load" (with optional list of file extensions);
wenzelm
parents:
48709
diff
changeset
|
138 |
type spec = (string * string list) * string list; |
46961
5c6955f487e5
outer syntax command definitions based on formal command_spec derived from theory header declarations;
wenzelm
parents:
46958
diff
changeset
|
139 |
|
48864
3ee314ae1e0a
added keyword kind "thy_load" (with optional list of file extensions);
wenzelm
parents:
48709
diff
changeset
|
140 |
fun spec ((name, files), tags) = |
3ee314ae1e0a
added keyword kind "thy_load" (with optional list of file extensions);
wenzelm
parents:
48709
diff
changeset
|
141 |
(case Symtab.lookup name_table name of |
3ee314ae1e0a
added keyword kind "thy_load" (with optional list of file extensions);
wenzelm
parents:
48709
diff
changeset
|
142 |
SOME kind => |
3ee314ae1e0a
added keyword kind "thy_load" (with optional list of file extensions);
wenzelm
parents:
48709
diff
changeset
|
143 |
let val kind' = kind |> fold tag tags in |
3ee314ae1e0a
added keyword kind "thy_load" (with optional list of file extensions);
wenzelm
parents:
48709
diff
changeset
|
144 |
if null files then kind' |
3ee314ae1e0a
added keyword kind "thy_load" (with optional list of file extensions);
wenzelm
parents:
48709
diff
changeset
|
145 |
else if name = kind_of thy_load then kind' |> add_files files |
3ee314ae1e0a
added keyword kind "thy_load" (with optional list of file extensions);
wenzelm
parents:
48709
diff
changeset
|
146 |
else error ("Illegal specification of files for " ^ quote name) |
3ee314ae1e0a
added keyword kind "thy_load" (with optional list of file extensions);
wenzelm
parents:
48709
diff
changeset
|
147 |
end |
3ee314ae1e0a
added keyword kind "thy_load" (with optional list of file extensions);
wenzelm
parents:
48709
diff
changeset
|
148 |
| NONE => error ("Unknown outer syntax keyword kind " ^ quote name)); |
46938
cda018294515
some support for outer syntax keyword declarations within theory header;
wenzelm
parents:
46924
diff
changeset
|
149 |
|
48646
91281e9472d8
more official command specifications, including source position;
wenzelm
parents:
46969
diff
changeset
|
150 |
fun command_spec ((name, s), pos) = ((name, spec s), pos); |
46961
5c6955f487e5
outer syntax command definitions based on formal command_spec derived from theory header declarations;
wenzelm
parents:
46958
diff
changeset
|
151 |
|
46938
cda018294515
some support for outer syntax keyword declarations within theory header;
wenzelm
parents:
46924
diff
changeset
|
152 |
|
27357
5b3a087ff292
moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents:
17270
diff
changeset
|
153 |
|
58903 | 154 |
(** keyword tables **) |
155 |
||
156 |
(* type keywords *) |
|
27357
5b3a087ff292
moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents:
17270
diff
changeset
|
157 |
|
48874
ff9cd47be39b
refined Thy_Load.check_thy: find more uses in body text, based on keywords;
wenzelm
parents:
48872
diff
changeset
|
158 |
datatype keywords = Keywords of |
58903 | 159 |
{minor: Scan.lexicon, |
160 |
major: Scan.lexicon, |
|
58906 | 161 |
commands: T Symtab.table}; |
58903 | 162 |
|
163 |
fun minor_keywords (Keywords {minor, ...}) = minor; |
|
164 |
fun major_keywords (Keywords {major, ...}) = major; |
|
58906 | 165 |
fun commands (Keywords {commands, ...}) = commands; |
58903 | 166 |
|
58906 | 167 |
fun make_keywords (minor, major, commands) = |
168 |
Keywords {minor = minor, major = major, commands = commands}; |
|
46957
0c15caf47040
clarified Keyword.is_keyword: union of minor and major;
wenzelm
parents:
46950
diff
changeset
|
169 |
|
58906 | 170 |
fun map_keywords f (Keywords {minor, major, commands}) = |
171 |
make_keywords (f (minor, major, commands)); |
|
58903 | 172 |
|
173 |
val empty_keywords = |
|
174 |
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
|
175 |
|
58903 | 176 |
fun merge_keywords |
58906 | 177 |
(Keywords {minor = minor1, major = major1, commands = commands1}, |
178 |
Keywords {minor = minor2, major = major2, commands = commands2}) = |
|
58903 | 179 |
make_keywords |
180 |
(Scan.merge_lexicons (minor1, minor2), |
|
181 |
Scan.merge_lexicons (major1, major2), |
|
58906 | 182 |
Symtab.merge (K true) (commands1, commands2)); |
27357
5b3a087ff292
moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents:
17270
diff
changeset
|
183 |
|
58903 | 184 |
val no_command_keywords = |
185 |
map_keywords (fn (minor, _, _) => (minor, Scan.empty_lexicon, Symtab.empty)); |
|
27357
5b3a087ff292
moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents:
17270
diff
changeset
|
186 |
|
58903 | 187 |
|
188 |
(* add keywords *) |
|
27357
5b3a087ff292
moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents:
17270
diff
changeset
|
189 |
|
58906 | 190 |
fun add (name, opt_kind) = map_keywords (fn (minor, major, commands) => |
58903 | 191 |
(case opt_kind of |
192 |
NONE => |
|
193 |
let |
|
194 |
val minor' = Scan.extend_lexicon (Symbol.explode name) minor; |
|
58906 | 195 |
in (minor', major, commands) end |
58903 | 196 |
| SOME kind => |
197 |
let |
|
198 |
val major' = Scan.extend_lexicon (Symbol.explode name) major; |
|
58906 | 199 |
val commands' = Symtab.update (name, kind) commands; |
200 |
in (minor, major', commands') end)); |
|
27357
5b3a087ff292
moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents:
17270
diff
changeset
|
201 |
|
58903 | 202 |
|
203 |
(* global state *) |
|
204 |
||
205 |
local val global_keywords = Unsynchronized.ref empty_keywords in |
|
206 |
||
207 |
fun define decl = CRITICAL (fn () => Unsynchronized.change global_keywords (add decl)); |
|
208 |
fun get_keywords () = ! global_keywords; |
|
27357
5b3a087ff292
moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents:
17270
diff
changeset
|
209 |
|
17059
a001a3ebfcfd
Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff
changeset
|
210 |
end; |
27357
5b3a087ff292
moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents:
17270
diff
changeset
|
211 |
|
58903 | 212 |
fun get_lexicons () = |
213 |
let val keywords = get_keywords () |
|
214 |
in (minor_keywords keywords, major_keywords keywords) end; |
|
215 |
||
58906 | 216 |
fun get_commands () = commands (get_keywords ()); |
46957
0c15caf47040
clarified Keyword.is_keyword: union of minor and major;
wenzelm
parents:
46950
diff
changeset
|
217 |
|
27357
5b3a087ff292
moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents:
17270
diff
changeset
|
218 |
|
5b3a087ff292
moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents:
17270
diff
changeset
|
219 |
(* lookup *) |
5b3a087ff292
moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents:
17270
diff
changeset
|
220 |
|
46957
0c15caf47040
clarified Keyword.is_keyword: union of minor and major;
wenzelm
parents:
46950
diff
changeset
|
221 |
fun is_keyword s = |
0c15caf47040
clarified Keyword.is_keyword: union of minor and major;
wenzelm
parents:
46950
diff
changeset
|
222 |
let |
0c15caf47040
clarified Keyword.is_keyword: union of minor and major;
wenzelm
parents:
46950
diff
changeset
|
223 |
val (minor, major) = get_lexicons (); |
0c15caf47040
clarified Keyword.is_keyword: union of minor and major;
wenzelm
parents:
46950
diff
changeset
|
224 |
val syms = Symbol.explode s; |
0c15caf47040
clarified Keyword.is_keyword: union of minor and major;
wenzelm
parents:
46950
diff
changeset
|
225 |
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
|
226 |
|
5b3a087ff292
moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents:
17270
diff
changeset
|
227 |
fun command_keyword name = Symtab.lookup (get_commands ()) name; |
54523 | 228 |
|
229 |
fun command_files name path = |
|
230 |
(case command_keyword name of |
|
231 |
NONE => [] |
|
232 |
| SOME (Keyword {kind, files, ...}) => |
|
233 |
if kind <> kind_of thy_load then [] |
|
234 |
else if null files then [path] |
|
235 |
else map (fn ext => Path.ext ext path) files); |
|
236 |
||
48867
e9beabf045ab
some support for inlining file content into outer syntax token language;
wenzelm
parents:
48864
diff
changeset
|
237 |
val command_tags = these o Option.map tags_of o command_keyword; |
27357
5b3a087ff292
moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents:
17270
diff
changeset
|
238 |
|
27433 | 239 |
|
28431 | 240 |
(* command categories *) |
27433 | 241 |
|
51225 | 242 |
fun command_category ks = |
243 |
let val tab = Symtab.make_set (map kind_of ks) in |
|
244 |
fn name => |
|
245 |
(case command_keyword name of |
|
246 |
NONE => false |
|
247 |
| SOME k => Symtab.defined tab (kind_of k)) |
|
248 |
end; |
|
27440
a1eda23752bd
replaced datatype category constructivism by is_theory/is_proof;
wenzelm
parents:
27433
diff
changeset
|
249 |
|
29347 | 250 |
val is_diag = command_category [diag]; |
40397 | 251 |
|
58868
c5e1cce7ace3
uniform heading commands work in any context, even in theory header;
wenzelm
parents:
58853
diff
changeset
|
252 |
val is_heading = command_category [heading]; |
29347 | 253 |
|
254 |
val is_theory_begin = command_category [thy_begin]; |
|
255 |
||
48867
e9beabf045ab
some support for inlining file content into outer syntax token language;
wenzelm
parents:
48864
diff
changeset
|
256 |
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
|
257 |
|
27440
a1eda23752bd
replaced datatype category constructivism by is_theory/is_proof;
wenzelm
parents:
27433
diff
changeset
|
258 |
val is_theory = command_category |
58868
c5e1cce7ace3
uniform heading commands work in any context, even in theory header;
wenzelm
parents:
58853
diff
changeset
|
259 |
[thy_begin, thy_end, thy_load, thy_decl, thy_decl_block, thy_goal]; |
27440
a1eda23752bd
replaced datatype category constructivism by is_theory/is_proof;
wenzelm
parents:
27433
diff
changeset
|
260 |
|
56944
578dc6b4be89
no reset for 'end' -- e.g. relevant for 'notepad';
wenzelm
parents:
56895
diff
changeset
|
261 |
val is_theory_body = command_category |
58868
c5e1cce7ace3
uniform heading commands work in any context, even in theory header;
wenzelm
parents:
58853
diff
changeset
|
262 |
[thy_load, thy_decl, thy_decl_block, thy_goal]; |
56944
578dc6b4be89
no reset for 'end' -- e.g. relevant for 'notepad';
wenzelm
parents:
56895
diff
changeset
|
263 |
|
27440
a1eda23752bd
replaced datatype category constructivism by is_theory/is_proof;
wenzelm
parents:
27433
diff
changeset
|
264 |
val is_proof = command_category |
58868
c5e1cce7ace3
uniform heading commands work in any context, even in theory header;
wenzelm
parents:
58853
diff
changeset
|
265 |
[qed, qed_script, qed_block, qed_global, prf_goal, prf_block, prf_open, prf_close, |
c5e1cce7ace3
uniform heading commands work in any context, even in theory header;
wenzelm
parents:
58853
diff
changeset
|
266 |
prf_chain, prf_decl, prf_asm, prf_asm_goal, prf_asm_goal_script, prf_script]; |
28431 | 267 |
|
51225 | 268 |
val is_proof_body = command_category |
58868
c5e1cce7ace3
uniform heading commands work in any context, even in theory header;
wenzelm
parents:
58853
diff
changeset
|
269 |
[diag, heading, prf_block, prf_open, prf_close, prf_chain, prf_decl, prf_asm, |
c5e1cce7ace3
uniform heading commands work in any context, even in theory header;
wenzelm
parents:
58853
diff
changeset
|
270 |
prf_asm_goal, prf_asm_goal_script, prf_script]; |
51225 | 271 |
|
51274
cfc83ad52571
discontinued pointless command category "thy_schematic_goal" -- this is checked dynamically;
wenzelm
parents:
51225
diff
changeset
|
272 |
val is_theory_goal = command_category [thy_goal]; |
53371
47b23c582127
more explicit indication of 'guess' as improper Isar (aka "script") element;
wenzelm
parents:
52440
diff
changeset
|
273 |
val is_proof_goal = command_category [prf_goal, prf_asm_goal, prf_asm_goal_script]; |
53571
e58ca0311c0f
more explicit indication of 'done' as proof script element;
wenzelm
parents:
53371
diff
changeset
|
274 |
val is_qed = command_category [qed, qed_script, qed_block]; |
28431 | 275 |
val is_qed_global = command_category [qed_global]; |
27520 | 276 |
|
56895
f058120aaad4
discontinued Toplevel.print flag -- print uniformly according to Keyword.is_printed;
wenzelm
parents:
56146
diff
changeset
|
277 |
val is_printed = is_theory_goal orf is_proof; |
f058120aaad4
discontinued Toplevel.print flag -- print uniformly according to Keyword.is_printed;
wenzelm
parents:
56146
diff
changeset
|
278 |
|
27357
5b3a087ff292
moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents:
17270
diff
changeset
|
279 |
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
|
280 |