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