author | wenzelm |
Wed, 02 Jul 2008 16:40:18 +0200 | |
changeset 27440 | a1eda23752bd |
parent 27433 | b82c12e57e79 |
child 27520 | fb07f3b32863 |
permissions | -rw-r--r-- |
17059
a001a3ebfcfd
Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff
changeset
|
1 |
(* Title: Pure/Isar/outer_keyword.ML |
a001a3ebfcfd
Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff
changeset
|
2 |
ID: $Id$ |
a001a3ebfcfd
Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff
changeset
|
3 |
Author: Makarius |
a001a3ebfcfd
Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff
changeset
|
4 |
|
27357
5b3a087ff292
moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents:
17270
diff
changeset
|
5 |
Isar command keyword classification and global keyword tables. |
17059
a001a3ebfcfd
Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff
changeset
|
6 |
*) |
a001a3ebfcfd
Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff
changeset
|
7 |
|
a001a3ebfcfd
Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff
changeset
|
8 |
signature OUTER_KEYWORD = |
a001a3ebfcfd
Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff
changeset
|
9 |
sig |
a001a3ebfcfd
Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff
changeset
|
10 |
type T |
a001a3ebfcfd
Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff
changeset
|
11 |
val kind_of: T -> string |
a001a3ebfcfd
Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff
changeset
|
12 |
val control: T |
a001a3ebfcfd
Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff
changeset
|
13 |
val diag: T |
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_switch: T |
a001a3ebfcfd
Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff
changeset
|
16 |
val thy_end: T |
a001a3ebfcfd
Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff
changeset
|
17 |
val thy_heading: T |
a001a3ebfcfd
Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff
changeset
|
18 |
val thy_decl: T |
a001a3ebfcfd
Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff
changeset
|
19 |
val thy_script: T |
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 |
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 update_tags: string -> string list -> string list |
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 |
27357
5b3a087ff292
moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents:
17270
diff
changeset
|
41 |
val get_lexicons: unit -> Scan.lexicon * Scan.lexicon |
5b3a087ff292
moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents:
17270
diff
changeset
|
42 |
val is_keyword: string -> bool |
5b3a087ff292
moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents:
17270
diff
changeset
|
43 |
val dest_keywords: unit -> string list |
5b3a087ff292
moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents:
17270
diff
changeset
|
44 |
val dest_commands: unit -> string list |
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 |
5b3a087ff292
moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents:
17270
diff
changeset
|
47 |
val report: unit -> unit |
5b3a087ff292
moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents:
17270
diff
changeset
|
48 |
val keyword: string -> unit |
5b3a087ff292
moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents:
17270
diff
changeset
|
49 |
val command: string -> T -> unit |
27440
a1eda23752bd
replaced datatype category constructivism by is_theory/is_proof;
wenzelm
parents:
27433
diff
changeset
|
50 |
val is_theory: string -> bool |
a1eda23752bd
replaced datatype category constructivism by is_theory/is_proof;
wenzelm
parents:
27433
diff
changeset
|
51 |
val is_proof: string -> bool |
17059
a001a3ebfcfd
Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff
changeset
|
52 |
end; |
a001a3ebfcfd
Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff
changeset
|
53 |
|
a001a3ebfcfd
Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff
changeset
|
54 |
structure OuterKeyword: OUTER_KEYWORD = |
a001a3ebfcfd
Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff
changeset
|
55 |
struct |
a001a3ebfcfd
Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff
changeset
|
56 |
|
27357
5b3a087ff292
moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents:
17270
diff
changeset
|
57 |
(** keyword classification **) |
17059
a001a3ebfcfd
Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff
changeset
|
58 |
|
a001a3ebfcfd
Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff
changeset
|
59 |
datatype T = Keyword of string * string list; |
a001a3ebfcfd
Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff
changeset
|
60 |
|
a001a3ebfcfd
Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff
changeset
|
61 |
fun kind s = Keyword (s, []); |
a001a3ebfcfd
Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff
changeset
|
62 |
fun kind_of (Keyword (s, _)) = s; |
a001a3ebfcfd
Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff
changeset
|
63 |
|
a001a3ebfcfd
Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff
changeset
|
64 |
|
a001a3ebfcfd
Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff
changeset
|
65 |
(* kinds *) |
a001a3ebfcfd
Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff
changeset
|
66 |
|
a001a3ebfcfd
Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff
changeset
|
67 |
val control = kind "control"; |
a001a3ebfcfd
Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff
changeset
|
68 |
val diag = kind "diag"; |
a001a3ebfcfd
Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff
changeset
|
69 |
val thy_begin = kind "theory-begin"; |
a001a3ebfcfd
Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff
changeset
|
70 |
val thy_switch = kind "theory-switch"; |
a001a3ebfcfd
Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff
changeset
|
71 |
val thy_end = kind "theory-end"; |
a001a3ebfcfd
Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff
changeset
|
72 |
val thy_heading = kind "theory-heading"; |
a001a3ebfcfd
Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff
changeset
|
73 |
val thy_decl = kind "theory-decl"; |
a001a3ebfcfd
Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff
changeset
|
74 |
val thy_script = kind "theory-script"; |
a001a3ebfcfd
Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff
changeset
|
75 |
val thy_goal = kind "theory-goal"; |
a001a3ebfcfd
Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff
changeset
|
76 |
val qed = kind "qed"; |
a001a3ebfcfd
Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff
changeset
|
77 |
val qed_block = kind "qed-block"; |
a001a3ebfcfd
Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff
changeset
|
78 |
val qed_global = kind "qed-global"; |
a001a3ebfcfd
Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff
changeset
|
79 |
val prf_heading = kind "proof-heading"; |
a001a3ebfcfd
Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff
changeset
|
80 |
val prf_goal = kind "proof-goal"; |
a001a3ebfcfd
Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff
changeset
|
81 |
val prf_block = kind "proof-block"; |
a001a3ebfcfd
Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff
changeset
|
82 |
val prf_open = kind "proof-open"; |
a001a3ebfcfd
Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff
changeset
|
83 |
val prf_close = kind "proof-close"; |
a001a3ebfcfd
Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff
changeset
|
84 |
val prf_chain = kind "proof-chain"; |
a001a3ebfcfd
Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff
changeset
|
85 |
val prf_decl = kind "proof-decl"; |
a001a3ebfcfd
Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff
changeset
|
86 |
val prf_asm = kind "proof-asm"; |
a001a3ebfcfd
Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff
changeset
|
87 |
val prf_asm_goal = kind "proof-asm-goal"; |
a001a3ebfcfd
Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff
changeset
|
88 |
val prf_script = kind "proof-script"; |
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 |
val kinds = [control, diag, thy_begin, thy_switch, thy_end, thy_heading, thy_decl, thy_script, |
a001a3ebfcfd
Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff
changeset
|
91 |
thy_goal, qed, qed_block, qed_global, prf_heading, prf_goal, prf_block, prf_open, prf_close, |
a001a3ebfcfd
Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff
changeset
|
92 |
prf_chain, prf_decl, prf_asm, prf_asm_goal, prf_script] |> map kind_of; |
a001a3ebfcfd
Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff
changeset
|
93 |
|
a001a3ebfcfd
Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff
changeset
|
94 |
|
a001a3ebfcfd
Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff
changeset
|
95 |
(* tags *) |
a001a3ebfcfd
Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff
changeset
|
96 |
|
17270 | 97 |
fun update_tags t ts = t :: remove (op = : string * string -> bool) t ts; |
17059
a001a3ebfcfd
Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff
changeset
|
98 |
|
a001a3ebfcfd
Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff
changeset
|
99 |
fun tag t (Keyword (s, ts)) = Keyword (s, update_tags t ts); |
a001a3ebfcfd
Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff
changeset
|
100 |
fun tags_of (Keyword (_, ts)) = ts; |
a001a3ebfcfd
Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff
changeset
|
101 |
|
a001a3ebfcfd
Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff
changeset
|
102 |
val tag_theory = tag "theory"; |
a001a3ebfcfd
Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff
changeset
|
103 |
val tag_proof = tag "proof"; |
a001a3ebfcfd
Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff
changeset
|
104 |
val tag_ml = tag "ML"; |
a001a3ebfcfd
Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff
changeset
|
105 |
|
27357
5b3a087ff292
moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents:
17270
diff
changeset
|
106 |
|
5b3a087ff292
moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents:
17270
diff
changeset
|
107 |
|
5b3a087ff292
moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents:
17270
diff
changeset
|
108 |
(** global keyword tables **) |
5b3a087ff292
moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents:
17270
diff
changeset
|
109 |
|
5b3a087ff292
moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents:
17270
diff
changeset
|
110 |
local |
5b3a087ff292
moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents:
17270
diff
changeset
|
111 |
|
5b3a087ff292
moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents:
17270
diff
changeset
|
112 |
val global_commands = ref (Symtab.empty: T Symtab.table); |
5b3a087ff292
moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents:
17270
diff
changeset
|
113 |
val global_lexicons = ref (Scan.empty_lexicon, Scan.empty_lexicon); |
5b3a087ff292
moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents:
17270
diff
changeset
|
114 |
|
5b3a087ff292
moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents:
17270
diff
changeset
|
115 |
in |
5b3a087ff292
moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents:
17270
diff
changeset
|
116 |
|
5b3a087ff292
moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents:
17270
diff
changeset
|
117 |
fun get_commands () = CRITICAL (fn () => ! global_commands); |
5b3a087ff292
moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents:
17270
diff
changeset
|
118 |
fun get_lexicons () = CRITICAL (fn () => ! global_lexicons); |
5b3a087ff292
moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents:
17270
diff
changeset
|
119 |
|
5b3a087ff292
moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents:
17270
diff
changeset
|
120 |
fun change_commands f = CRITICAL (fn () => change global_commands f); |
5b3a087ff292
moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents:
17270
diff
changeset
|
121 |
|
5b3a087ff292
moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents:
17270
diff
changeset
|
122 |
fun change_lexicons f = CRITICAL (fn () => |
5b3a087ff292
moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents:
17270
diff
changeset
|
123 |
(change global_lexicons f; |
5b3a087ff292
moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents:
17270
diff
changeset
|
124 |
(case (op inter_string) (pairself Scan.dest_lexicon (get_lexicons ())) of |
5b3a087ff292
moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents:
17270
diff
changeset
|
125 |
[] => () |
5b3a087ff292
moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents:
17270
diff
changeset
|
126 |
| clash => warning ("Overlapping outer syntax commands and keywords: " ^ commas_quote clash)))); |
5b3a087ff292
moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents:
17270
diff
changeset
|
127 |
|
17059
a001a3ebfcfd
Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff
changeset
|
128 |
end; |
27357
5b3a087ff292
moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents:
17270
diff
changeset
|
129 |
|
5b3a087ff292
moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents:
17270
diff
changeset
|
130 |
|
5b3a087ff292
moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents:
17270
diff
changeset
|
131 |
(* lookup *) |
5b3a087ff292
moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents:
17270
diff
changeset
|
132 |
|
5b3a087ff292
moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents:
17270
diff
changeset
|
133 |
fun is_keyword s = Scan.is_literal (#1 (get_lexicons ())) (Symbol.explode s); |
5b3a087ff292
moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents:
17270
diff
changeset
|
134 |
fun dest_keywords () = Scan.dest_lexicon (#1 (get_lexicons ())); |
5b3a087ff292
moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents:
17270
diff
changeset
|
135 |
|
5b3a087ff292
moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents:
17270
diff
changeset
|
136 |
fun dest_commands () = Symtab.keys (get_commands ()); |
5b3a087ff292
moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents:
17270
diff
changeset
|
137 |
fun command_keyword name = Symtab.lookup (get_commands ()) name; |
5b3a087ff292
moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents:
17270
diff
changeset
|
138 |
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
|
139 |
|
5b3a087ff292
moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents:
17270
diff
changeset
|
140 |
|
5b3a087ff292
moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents:
17270
diff
changeset
|
141 |
(* report *) |
5b3a087ff292
moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents:
17270
diff
changeset
|
142 |
|
5b3a087ff292
moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents:
17270
diff
changeset
|
143 |
fun report_keyword name = |
5b3a087ff292
moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents:
17270
diff
changeset
|
144 |
Pretty.mark (Markup.keyword_decl name) |
5b3a087ff292
moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents:
17270
diff
changeset
|
145 |
(Pretty.str ("Outer syntax keyword: " ^ quote name)); |
5b3a087ff292
moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents:
17270
diff
changeset
|
146 |
|
5b3a087ff292
moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents:
17270
diff
changeset
|
147 |
fun report_command (name, kind) = |
5b3a087ff292
moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents:
17270
diff
changeset
|
148 |
Pretty.mark (Markup.command_decl name (kind_of kind)) |
5b3a087ff292
moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents:
17270
diff
changeset
|
149 |
(Pretty.str ("Outer syntax command: " ^ quote name ^ " (" ^ kind_of kind ^ ")")); |
5b3a087ff292
moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents:
17270
diff
changeset
|
150 |
|
5b3a087ff292
moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents:
17270
diff
changeset
|
151 |
fun report () = |
5b3a087ff292
moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents:
17270
diff
changeset
|
152 |
let val (keywords, commands) = CRITICAL (fn () => |
5b3a087ff292
moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents:
17270
diff
changeset
|
153 |
(dest_keywords (), Symtab.dest (get_commands ()))) |
5b3a087ff292
moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents:
17270
diff
changeset
|
154 |
in map report_keyword keywords @ map report_command commands end |
5b3a087ff292
moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents:
17270
diff
changeset
|
155 |
|> Pretty.chunks |> Pretty.writeln; |
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 |
|
5b3a087ff292
moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents:
17270
diff
changeset
|
158 |
(* augment tables *) |
5b3a087ff292
moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents:
17270
diff
changeset
|
159 |
|
5b3a087ff292
moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents:
17270
diff
changeset
|
160 |
fun keyword name = |
5b3a087ff292
moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents:
17270
diff
changeset
|
161 |
(change_lexicons (apfst (Scan.extend_lexicon [Symbol.explode name])); |
5b3a087ff292
moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents:
17270
diff
changeset
|
162 |
Pretty.writeln (report_keyword name)); |
5b3a087ff292
moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents:
17270
diff
changeset
|
163 |
|
5b3a087ff292
moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents:
17270
diff
changeset
|
164 |
fun command name kind = |
5b3a087ff292
moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents:
17270
diff
changeset
|
165 |
(change_lexicons (apsnd (Scan.extend_lexicon [Symbol.explode name])); |
5b3a087ff292
moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents:
17270
diff
changeset
|
166 |
change_commands (Symtab.update (name, kind)); |
5b3a087ff292
moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents:
17270
diff
changeset
|
167 |
Pretty.writeln (report_command (name, kind))); |
5b3a087ff292
moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents:
17270
diff
changeset
|
168 |
|
27433 | 169 |
|
170 |
(* overall category *) |
|
171 |
||
27440
a1eda23752bd
replaced datatype category constructivism by is_theory/is_proof;
wenzelm
parents:
27433
diff
changeset
|
172 |
fun command_category ks name = |
27433 | 173 |
(case command_keyword name of |
27440
a1eda23752bd
replaced datatype category constructivism by is_theory/is_proof;
wenzelm
parents:
27433
diff
changeset
|
174 |
NONE => false |
a1eda23752bd
replaced datatype category constructivism by is_theory/is_proof;
wenzelm
parents:
27433
diff
changeset
|
175 |
| SOME k => member (op =) ks (kind_of k)); |
a1eda23752bd
replaced datatype category constructivism by is_theory/is_proof;
wenzelm
parents:
27433
diff
changeset
|
176 |
|
a1eda23752bd
replaced datatype category constructivism by is_theory/is_proof;
wenzelm
parents:
27433
diff
changeset
|
177 |
val is_theory = command_category |
a1eda23752bd
replaced datatype category constructivism by is_theory/is_proof;
wenzelm
parents:
27433
diff
changeset
|
178 |
(map kind_of [thy_begin, thy_switch, thy_end, thy_heading, thy_decl, thy_script, thy_goal]); |
a1eda23752bd
replaced datatype category constructivism by is_theory/is_proof;
wenzelm
parents:
27433
diff
changeset
|
179 |
|
a1eda23752bd
replaced datatype category constructivism by is_theory/is_proof;
wenzelm
parents:
27433
diff
changeset
|
180 |
val is_proof = command_category |
a1eda23752bd
replaced datatype category constructivism by is_theory/is_proof;
wenzelm
parents:
27433
diff
changeset
|
181 |
(map kind_of [qed, qed_block, qed_global, prf_heading, prf_goal, prf_block, prf_open, prf_close, |
a1eda23752bd
replaced datatype category constructivism by is_theory/is_proof;
wenzelm
parents:
27433
diff
changeset
|
182 |
prf_chain, prf_decl, prf_asm, prf_asm_goal, prf_script]); |
27433 | 183 |
|
27357
5b3a087ff292
moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents:
17270
diff
changeset
|
184 |
end; |