1(* Title: Pure/Isar/keyword.ML 2 Author: Makarius 3 4Isar keyword classification. 5*) 6 7signature KEYWORD = 8sig 9 val diag: string 10 val document_heading: string 11 val document_body: string 12 val document_raw: string 13 val thy_begin: string 14 val thy_end: string 15 val thy_decl: string 16 val thy_decl_block: string 17 val thy_load: string 18 val thy_goal: string 19 val qed: string 20 val qed_script: string 21 val qed_block: string 22 val qed_global: string 23 val prf_goal: string 24 val prf_block: string 25 val next_block: string 26 val prf_open: string 27 val prf_close: string 28 val prf_chain: string 29 val prf_decl: string 30 val prf_asm: string 31 val prf_asm_goal: string 32 val prf_script: string 33 val prf_script_goal: string 34 val prf_script_asm_goal: string 35 val before_command: string 36 val quasi_command: string 37 type spec = (string * string list) * string list 38 val no_spec: spec 39 val before_command_spec: spec 40 val quasi_command_spec: spec 41 val document_heading_spec: spec 42 val document_body_spec: spec 43 type keywords 44 val minor_keywords: keywords -> Scan.lexicon 45 val major_keywords: keywords -> Scan.lexicon 46 val no_command_keywords: keywords -> keywords 47 val empty_keywords: keywords 48 val merge_keywords: keywords * keywords -> keywords 49 val add_keywords: ((string * Position.T) * spec) list -> keywords -> keywords 50 val is_keyword: keywords -> string -> bool 51 val is_command: keywords -> string -> bool 52 val is_literal: keywords -> string -> bool 53 val dest_commands: keywords -> string list 54 val command_markup: keywords -> string -> Markup.T option 55 val command_kind: keywords -> string -> string option 56 val command_files: keywords -> string -> Path.T -> Path.T list 57 val command_tags: keywords -> string -> string list 58 val is_vacuous: keywords -> string -> bool 59 val is_diag: keywords -> string -> bool 60 val is_document_heading: keywords -> string -> bool 61 val is_document_body: keywords -> string -> bool 62 val is_document_raw: keywords -> string -> bool 63 val is_document: keywords -> string -> bool 64 val is_theory_end: keywords -> string -> bool 65 val is_theory_load: keywords -> string -> bool 66 val is_theory: keywords -> string -> bool 67 val is_theory_body: keywords -> string -> bool 68 val is_proof: keywords -> string -> bool 69 val is_proof_body: keywords -> string -> bool 70 val is_theory_goal: keywords -> string -> bool 71 val is_proof_goal: keywords -> string -> bool 72 val is_qed: keywords -> string -> bool 73 val is_qed_global: keywords -> string -> bool 74 val is_proof_open: keywords -> string -> bool 75 val is_proof_close: keywords -> string -> bool 76 val is_proof_asm: keywords -> string -> bool 77 val is_improper: keywords -> string -> bool 78 val is_printed: keywords -> string -> bool 79end; 80 81structure Keyword: KEYWORD = 82struct 83 84(** keyword classification **) 85 86(* kinds *) 87 88val diag = "diag"; 89val document_heading = "document_heading"; 90val document_body = "document_body"; 91val document_raw = "document_raw"; 92val thy_begin = "thy_begin"; 93val thy_end = "thy_end"; 94val thy_decl = "thy_decl"; 95val thy_decl_block = "thy_decl_block"; 96val thy_load = "thy_load"; 97val thy_goal = "thy_goal"; 98val qed = "qed"; 99val qed_script = "qed_script"; 100val qed_block = "qed_block"; 101val qed_global = "qed_global"; 102val prf_goal = "prf_goal"; 103val prf_block = "prf_block"; 104val next_block = "next_block"; 105val prf_open = "prf_open"; 106val prf_close = "prf_close"; 107val prf_chain = "prf_chain"; 108val prf_decl = "prf_decl"; 109val prf_asm = "prf_asm"; 110val prf_asm_goal = "prf_asm_goal"; 111val prf_script = "prf_script"; 112val prf_script_goal = "prf_script_goal"; 113val prf_script_asm_goal = "prf_script_asm_goal"; 114 115val before_command = "before_command"; 116val quasi_command = "quasi_command"; 117 118val command_kinds = 119 [diag, document_heading, document_body, document_raw, thy_begin, thy_end, thy_load, thy_decl, 120 thy_decl_block, thy_goal, qed, qed_script, qed_block, qed_global, prf_goal, prf_block, 121 next_block, prf_open, prf_close, prf_chain, prf_decl, prf_asm, prf_asm_goal, prf_script, 122 prf_script_goal, prf_script_asm_goal]; 123 124 125(* specifications *) 126 127type spec = (string * string list) * string list; 128 129val no_spec: spec = (("", []), []); 130val before_command_spec: spec = ((before_command, []), []); 131val quasi_command_spec: spec = ((quasi_command, []), []); 132val document_heading_spec: spec = (("document_heading", []), ["document"]); 133val document_body_spec: spec = (("document_body", []), ["document"]); 134 135type entry = 136 {pos: Position.T, 137 id: serial, 138 kind: string, 139 files: string list, (*extensions of embedded files*) 140 tags: string list}; 141 142fun check_spec pos ((kind, files), tags) : entry = 143 if not (member (op =) command_kinds kind) then 144 error ("Unknown outer syntax keyword kind " ^ quote kind) 145 else if not (null files) andalso kind <> thy_load then 146 error ("Illegal specification of files for " ^ quote kind) 147 else {pos = pos, id = serial (), kind = kind, files = files, tags = tags}; 148 149 150(** keyword tables **) 151 152(* type keywords *) 153 154datatype keywords = Keywords of 155 {minor: Scan.lexicon, 156 major: Scan.lexicon, 157 commands: entry Symtab.table}; 158 159fun minor_keywords (Keywords {minor, ...}) = minor; 160fun major_keywords (Keywords {major, ...}) = major; 161 162fun make_keywords (minor, major, commands) = 163 Keywords {minor = minor, major = major, commands = commands}; 164 165fun map_keywords f (Keywords {minor, major, commands}) = 166 make_keywords (f (minor, major, commands)); 167 168val no_command_keywords = 169 map_keywords (fn (minor, _, _) => (minor, Scan.empty_lexicon, Symtab.empty)); 170 171 172(* build keywords *) 173 174val empty_keywords = 175 make_keywords (Scan.empty_lexicon, Scan.empty_lexicon, Symtab.empty); 176 177fun merge_keywords 178 (Keywords {minor = minor1, major = major1, commands = commands1}, 179 Keywords {minor = minor2, major = major2, commands = commands2}) = 180 make_keywords 181 (Scan.merge_lexicons (minor1, minor2), 182 Scan.merge_lexicons (major1, major2), 183 Symtab.merge (K true) (commands1, commands2)); 184 185val add_keywords = 186 fold (fn ((name, pos), spec as ((kind, _), _)) => map_keywords (fn (minor, major, commands) => 187 if kind = "" orelse kind = before_command orelse kind = quasi_command then 188 let 189 val minor' = Scan.extend_lexicon (Symbol.explode name) minor; 190 in (minor', major, commands) end 191 else 192 let 193 val entry = check_spec pos spec; 194 val major' = Scan.extend_lexicon (Symbol.explode name) major; 195 val commands' = Symtab.update (name, entry) commands; 196 in (minor, major', commands') end)); 197 198 199(* keyword status *) 200 201fun is_keyword keywords s = Scan.is_literal (minor_keywords keywords) (Symbol.explode s); 202fun is_command (Keywords {commands, ...}) = Symtab.defined commands; 203fun is_literal keywords = is_keyword keywords orf is_command keywords; 204 205fun dest_commands (Keywords {commands, ...}) = Symtab.keys commands; 206 207 208(* command keywords *) 209 210fun lookup_command (Keywords {commands, ...}) = Symtab.lookup commands; 211 212fun command_markup keywords name = 213 lookup_command keywords name 214 |> Option.map (fn {pos, id, ...} => 215 Markup.properties (Position.entity_properties_of false id pos) 216 (Markup.entity Markup.command_keywordN name)); 217 218fun command_kind keywords = Option.map #kind o lookup_command keywords; 219 220fun command_files keywords name path = 221 (case lookup_command keywords name of 222 NONE => [] 223 | SOME {kind, files, ...} => 224 if kind <> thy_load then [] 225 else if null files then [path] 226 else map (fn ext => Path.ext ext path) files); 227 228fun command_tags keywords name = 229 (case lookup_command keywords name of 230 SOME {tags, ...} => tags 231 | NONE => []); 232 233 234(* command categories *) 235 236fun command_category ks = 237 let 238 val tab = Symtab.make_set ks; 239 fun pred keywords name = 240 (case lookup_command keywords name of 241 NONE => false 242 | SOME {kind, ...} => Symtab.defined tab kind); 243 in pred end; 244 245val is_vacuous = command_category [diag, document_heading, document_body, document_raw]; 246 247val is_diag = command_category [diag]; 248 249val is_document_heading = command_category [document_heading]; 250val is_document_body = command_category [document_body]; 251val is_document_raw = command_category [document_raw]; 252val is_document = command_category [document_heading, document_body, document_raw]; 253 254val is_theory_end = command_category [thy_end]; 255 256val is_theory_load = command_category [thy_load]; 257 258val is_theory = command_category 259 [thy_begin, thy_end, thy_load, thy_decl, thy_decl_block, thy_goal]; 260 261val is_theory_body = command_category 262 [thy_load, thy_decl, thy_decl_block, thy_goal]; 263 264val is_proof = command_category 265 [qed, qed_script, qed_block, qed_global, prf_goal, prf_block, next_block, prf_open, 266 prf_close, prf_chain, prf_decl, prf_asm, prf_asm_goal, prf_script, prf_script_goal, 267 prf_script_asm_goal]; 268 269val is_proof_body = command_category 270 [diag, document_heading, document_body, document_raw, prf_block, next_block, prf_open, 271 prf_close, prf_chain, prf_decl, prf_asm, prf_asm_goal, prf_script, prf_script_goal, 272 prf_script_asm_goal]; 273 274val is_theory_goal = command_category [thy_goal]; 275val is_proof_goal = command_category [prf_goal, prf_asm_goal, prf_script_goal, prf_script_asm_goal]; 276val is_qed = command_category [qed, qed_script, qed_block]; 277val is_qed_global = command_category [qed_global]; 278 279val is_proof_open = 280 command_category [prf_goal, prf_asm_goal, prf_script_goal, prf_script_asm_goal, prf_open]; 281val is_proof_close = command_category [qed, qed_script, qed_block, prf_close]; 282 283val is_proof_asm = command_category [prf_asm, prf_asm_goal]; 284val is_improper = command_category [qed_script, prf_script, prf_script_goal, prf_script_asm_goal]; 285 286fun is_printed keywords = is_theory_goal keywords orf is_proof keywords; 287 288end; 289