1191783Srmacklem(* Title: Pure/Isar/keyword.ML 2191783Srmacklem Author: Makarius 3191783Srmacklem 4191783SrmacklemIsar keyword classification. 5191783Srmacklem*) 6191783Srmacklem 7191783Srmacklemsignature KEYWORD = 8191783Srmacklemsig 9191783Srmacklem val diag: string 10191783Srmacklem val document_heading: string 11191783Srmacklem val document_body: string 12191783Srmacklem val document_raw: string 13191783Srmacklem val thy_begin: string 14191783Srmacklem val thy_end: string 15191783Srmacklem val thy_decl: string 16191783Srmacklem val thy_decl_block: string 17191783Srmacklem val thy_load: string 18191783Srmacklem val thy_goal: string 19191783Srmacklem val qed: string 20191783Srmacklem val qed_script: string 21191783Srmacklem val qed_block: string 22191783Srmacklem val qed_global: string 23191783Srmacklem val prf_goal: string 24191783Srmacklem val prf_block: string 25191783Srmacklem val next_block: string 26191783Srmacklem val prf_open: string 27191783Srmacklem val prf_close: string 28191783Srmacklem val prf_chain: string 29191783Srmacklem val prf_decl: string 30191783Srmacklem val prf_asm: string 31191783Srmacklem val prf_asm_goal: string 32191783Srmacklem val prf_script: string 33191783Srmacklem val prf_script_goal: string 34191783Srmacklem val prf_script_asm_goal: string 35191783Srmacklem val before_command: string 36191783Srmacklem val quasi_command: string 37191783Srmacklem type spec = (string * string list) * string list 38191783Srmacklem val no_spec: spec 39191783Srmacklem val before_command_spec: spec 40191783Srmacklem val quasi_command_spec: spec 41191783Srmacklem val document_heading_spec: spec 42191783Srmacklem val document_body_spec: spec 43191783Srmacklem type keywords 44191783Srmacklem val minor_keywords: keywords -> Scan.lexicon 45191783Srmacklem val major_keywords: keywords -> Scan.lexicon 46191783Srmacklem val no_command_keywords: keywords -> keywords 47191783Srmacklem val empty_keywords: keywords 48191783Srmacklem val merge_keywords: keywords * keywords -> keywords 49191783Srmacklem val add_keywords: ((string * Position.T) * spec) list -> keywords -> keywords 50191783Srmacklem val is_keyword: keywords -> string -> bool 51191783Srmacklem val is_command: keywords -> string -> bool 52191783Srmacklem val is_literal: keywords -> string -> bool 53191783Srmacklem val dest_commands: keywords -> string list 54191783Srmacklem val command_markup: keywords -> string -> Markup.T option 55191783Srmacklem val command_kind: keywords -> string -> string option 56191783Srmacklem val command_files: keywords -> string -> Path.T -> Path.T list 57191783Srmacklem val command_tags: keywords -> string -> string list 58191783Srmacklem val is_vacuous: keywords -> string -> bool 59191783Srmacklem val is_diag: keywords -> string -> bool 60191783Srmacklem val is_document_heading: keywords -> string -> bool 61191783Srmacklem val is_document_body: keywords -> string -> bool 62191783Srmacklem val is_document_raw: keywords -> string -> bool 63191783Srmacklem val is_document: keywords -> string -> bool 64191783Srmacklem val is_theory_end: keywords -> string -> bool 65191783Srmacklem val is_theory_load: keywords -> string -> bool 66191783Srmacklem val is_theory: keywords -> string -> bool 67191783Srmacklem val is_theory_body: keywords -> string -> bool 68191783Srmacklem val is_proof: keywords -> string -> bool 69191783Srmacklem val is_proof_body: keywords -> string -> bool 70191783Srmacklem val is_theory_goal: keywords -> string -> bool 71191783Srmacklem val is_proof_goal: keywords -> string -> bool 72191783Srmacklem val is_qed: keywords -> string -> bool 73191783Srmacklem val is_qed_global: keywords -> string -> bool 74191783Srmacklem val is_proof_open: keywords -> string -> bool 75191783Srmacklem val is_proof_close: keywords -> string -> bool 76191783Srmacklem val is_proof_asm: keywords -> string -> bool 77191783Srmacklem val is_improper: keywords -> string -> bool 78191783Srmacklem val is_printed: keywords -> string -> bool 79191783Srmacklemend; 80191783Srmacklem 81191783Srmacklemstructure Keyword: KEYWORD = 82191783Srmacklemstruct 83191783Srmacklem 84191783Srmacklem(** keyword classification **) 85191783Srmacklem 86191783Srmacklem(* kinds *) 87192115Srmacklem 88191783Srmacklemval diag = "diag"; 89191783Srmacklemval document_heading = "document_heading"; 90191783Srmacklemval document_body = "document_body"; 91191783Srmacklemval document_raw = "document_raw"; 92191783Srmacklemval thy_begin = "thy_begin"; 93191783Srmacklemval thy_end = "thy_end"; 94191783Srmacklemval thy_decl = "thy_decl"; 95191783Srmacklemval thy_decl_block = "thy_decl_block"; 96191783Srmacklemval thy_load = "thy_load"; 97191783Srmacklemval thy_goal = "thy_goal"; 98191783Srmacklemval qed = "qed"; 99191783Srmacklemval qed_script = "qed_script"; 100191783Srmacklemval qed_block = "qed_block"; 101191783Srmacklemval qed_global = "qed_global"; 102191783Srmacklemval prf_goal = "prf_goal"; 103191783Srmacklemval prf_block = "prf_block"; 104191783Srmacklemval next_block = "next_block"; 105191783Srmacklemval prf_open = "prf_open"; 106191783Srmacklemval prf_close = "prf_close"; 107191783Srmacklemval prf_chain = "prf_chain"; 108191783Srmacklemval prf_decl = "prf_decl"; 109191783Srmacklemval prf_asm = "prf_asm"; 110191783Srmacklemval prf_asm_goal = "prf_asm_goal"; 111191783Srmacklemval prf_script = "prf_script"; 112191783Srmacklemval prf_script_goal = "prf_script_goal"; 113191783Srmacklemval prf_script_asm_goal = "prf_script_asm_goal"; 114191783Srmacklem 115191783Srmacklemval before_command = "before_command"; 116191783Srmacklemval quasi_command = "quasi_command"; 117191783Srmacklem 118191783Srmacklemval command_kinds = 119191783Srmacklem [diag, document_heading, document_body, document_raw, thy_begin, thy_end, thy_load, thy_decl, 120191783Srmacklem thy_decl_block, thy_goal, qed, qed_script, qed_block, qed_global, prf_goal, prf_block, 121191783Srmacklem next_block, prf_open, prf_close, prf_chain, prf_decl, prf_asm, prf_asm_goal, prf_script, 122191783Srmacklem prf_script_goal, prf_script_asm_goal]; 123191783Srmacklem 124191783Srmacklem 125191783Srmacklem(* specifications *) 126220530Srmacklem 127191783Srmacklemtype spec = (string * string list) * string list; 128192115Srmacklem 129191783Srmacklemval no_spec: spec = (("", []), []); 130191783Srmacklemval before_command_spec: spec = ((before_command, []), []); 131191783Srmacklemval quasi_command_spec: spec = ((quasi_command, []), []); 132191783Srmacklemval document_heading_spec: spec = (("document_heading", []), ["document"]); 133191783Srmacklemval document_body_spec: spec = (("document_body", []), ["document"]); 134191783Srmacklem 135191783Srmacklemtype entry = 136191783Srmacklem {pos: Position.T, 137191783Srmacklem id: serial, 138191783Srmacklem kind: string, 139191783Srmacklem files: string list, (*extensions of embedded files*) 140191783Srmacklem tags: string list}; 141191783Srmacklem 142191783Srmacklemfun check_spec pos ((kind, files), tags) : entry = 143191783Srmacklem if not (member (op =) command_kinds kind) then 144191783Srmacklem error ("Unknown outer syntax keyword kind " ^ quote kind) 145191783Srmacklem else if not (null files) andalso kind <> thy_load then 146191783Srmacklem error ("Illegal specification of files for " ^ quote kind) 147191783Srmacklem else {pos = pos, id = serial (), kind = kind, files = files, tags = tags}; 148191783Srmacklem 149191783Srmacklem 150191783Srmacklem(** keyword tables **) 151191783Srmacklem 152191783Srmacklem(* type keywords *) 153191783Srmacklem 154191783Srmacklemdatatype keywords = Keywords of 155191783Srmacklem {minor: Scan.lexicon, 156191783Srmacklem major: Scan.lexicon, 157191783Srmacklem commands: entry Symtab.table}; 158191783Srmacklem 159191783Srmacklemfun minor_keywords (Keywords {minor, ...}) = minor; 160191783Srmacklemfun major_keywords (Keywords {major, ...}) = major; 161191783Srmacklem 162191783Srmacklemfun make_keywords (minor, major, commands) = 163191783Srmacklem Keywords {minor = minor, major = major, commands = commands}; 164191783Srmacklem 165191783Srmacklemfun map_keywords f (Keywords {minor, major, commands}) = 166191783Srmacklem make_keywords (f (minor, major, commands)); 167191783Srmacklem 168191783Srmacklemval no_command_keywords = 169191783Srmacklem map_keywords (fn (minor, _, _) => (minor, Scan.empty_lexicon, Symtab.empty)); 170191783Srmacklem 171191783Srmacklem 172191783Srmacklem(* build keywords *) 173191783Srmacklem 174191783Srmacklemval empty_keywords = 175191783Srmacklem make_keywords (Scan.empty_lexicon, Scan.empty_lexicon, Symtab.empty); 176191783Srmacklem 177191783Srmacklemfun merge_keywords 178191783Srmacklem (Keywords {minor = minor1, major = major1, commands = commands1}, 179191783Srmacklem Keywords {minor = minor2, major = major2, commands = commands2}) = 180191783Srmacklem make_keywords 181191783Srmacklem (Scan.merge_lexicons (minor1, minor2), 182191783Srmacklem Scan.merge_lexicons (major1, major2), 183191783Srmacklem Symtab.merge (K true) (commands1, commands2)); 184191783Srmacklem 185191783Srmacklemval add_keywords = 186191783Srmacklem fold (fn ((name, pos), spec as ((kind, _), _)) => map_keywords (fn (minor, major, commands) => 187191783Srmacklem if kind = "" orelse kind = before_command orelse kind = quasi_command then 188191783Srmacklem let 189191783Srmacklem val minor' = Scan.extend_lexicon (Symbol.explode name) minor; 190191783Srmacklem in (minor', major, commands) end 191191783Srmacklem else 192191783Srmacklem let 193191783Srmacklem val entry = check_spec pos spec; 194191783Srmacklem val major' = Scan.extend_lexicon (Symbol.explode name) major; 195191783Srmacklem val commands' = Symtab.update (name, entry) commands; 196191783Srmacklem in (minor, major', commands') end)); 197191783Srmacklem 198191783Srmacklem 199191783Srmacklem(* keyword status *) 200191783Srmacklem 201191783Srmacklemfun is_keyword keywords s = Scan.is_literal (minor_keywords keywords) (Symbol.explode s); 202191783Srmacklemfun is_command (Keywords {commands, ...}) = Symtab.defined commands; 203191783Srmacklemfun is_literal keywords = is_keyword keywords orf is_command keywords; 204191783Srmacklem 205191783Srmacklemfun dest_commands (Keywords {commands, ...}) = Symtab.keys commands; 206191783Srmacklem 207191783Srmacklem 208191783Srmacklem(* command keywords *) 209191783Srmacklem 210191783Srmacklemfun lookup_command (Keywords {commands, ...}) = Symtab.lookup commands; 211191783Srmacklem 212192115Srmacklemfun command_markup keywords name = 213191783Srmacklem lookup_command keywords name 214191783Srmacklem |> Option.map (fn {pos, id, ...} => 215191783Srmacklem Markup.properties (Position.entity_properties_of false id pos) 216192115Srmacklem (Markup.entity Markup.command_keywordN name)); 217191783Srmacklem 218191783Srmacklemfun command_kind keywords = Option.map #kind o lookup_command keywords; 219191783Srmacklem 220191783Srmacklemfun command_files keywords name path = 221191783Srmacklem (case lookup_command keywords name of 222191783Srmacklem NONE => [] 223191783Srmacklem | SOME {kind, files, ...} => 224191783Srmacklem if kind <> thy_load then [] 225191783Srmacklem else if null files then [path] 226191783Srmacklem else map (fn ext => Path.ext ext path) files); 227192115Srmacklem 228191783Srmacklemfun command_tags keywords name = 229191783Srmacklem (case lookup_command keywords name of 230191783Srmacklem SOME {tags, ...} => tags 231191783Srmacklem | NONE => []); 232191783Srmacklem 233191783Srmacklem 234191783Srmacklem(* command categories *) 235191783Srmacklem 236191783Srmacklemfun command_category ks = 237191783Srmacklem let 238191783Srmacklem val tab = Symtab.make_set ks; 239191783Srmacklem fun pred keywords name = 240191783Srmacklem (case lookup_command keywords name of 241191783Srmacklem NONE => false 242191783Srmacklem | SOME {kind, ...} => Symtab.defined tab kind); 243191783Srmacklem in pred end; 244191783Srmacklem 245191783Srmacklemval is_vacuous = command_category [diag, document_heading, document_body, document_raw]; 246191783Srmacklem 247191783Srmacklemval is_diag = command_category [diag]; 248191783Srmacklem 249191783Srmacklemval is_document_heading = command_category [document_heading]; 250222389Srmacklemval is_document_body = command_category [document_body]; 251191783Srmacklemval is_document_raw = command_category [document_raw]; 252191783Srmacklemval is_document = command_category [document_heading, document_body, document_raw]; 253222389Srmacklem 254211951Srmacklemval is_theory_end = command_category [thy_end]; 255205941Srmacklem 256191783Srmacklemval is_theory_load = command_category [thy_load]; 257191783Srmacklem 258192115Srmacklemval is_theory = command_category 259192115Srmacklem [thy_begin, thy_end, thy_load, thy_decl, thy_decl_block, thy_goal]; 260191783Srmacklem 261192115Srmacklemval is_theory_body = command_category 262191783Srmacklem [thy_load, thy_decl, thy_decl_block, thy_goal]; 263191783Srmacklem 264191783Srmacklemval is_proof = command_category 265191783Srmacklem [qed, qed_script, qed_block, qed_global, prf_goal, prf_block, next_block, prf_open, 266191783Srmacklem prf_close, prf_chain, prf_decl, prf_asm, prf_asm_goal, prf_script, prf_script_goal, 267191783Srmacklem prf_script_asm_goal]; 268191783Srmacklem 269191783Srmacklemval is_proof_body = command_category 270191783Srmacklem [diag, document_heading, document_body, document_raw, prf_block, next_block, prf_open, 271191783Srmacklem prf_close, prf_chain, prf_decl, prf_asm, prf_asm_goal, prf_script, prf_script_goal, 272191783Srmacklem prf_script_asm_goal]; 273191783Srmacklem 274191783Srmacklemval is_theory_goal = command_category [thy_goal]; 275191783Srmacklemval is_proof_goal = command_category [prf_goal, prf_asm_goal, prf_script_goal, prf_script_asm_goal]; 276191783Srmacklemval is_qed = command_category [qed, qed_script, qed_block]; 277191783Srmacklemval is_qed_global = command_category [qed_global]; 278191783Srmacklem 279191783Srmacklemval is_proof_open = 280191783Srmacklem command_category [prf_goal, prf_asm_goal, prf_script_goal, prf_script_asm_goal, prf_open]; 281192115Srmacklemval is_proof_close = command_category [qed, qed_script, qed_block, prf_close]; 282216700Srmacklem 283191783Srmacklemval is_proof_asm = command_category [prf_asm, prf_asm_goal]; 284191783Srmacklemval is_improper = command_category [qed_script, prf_script, prf_script_goal, prf_script_asm_goal]; 285191783Srmacklem 286191783Srmacklemfun is_printed keywords = is_theory_goal keywords orf is_proof keywords; 287191783Srmacklem 288191783Srmacklemend; 289191783Srmacklem