src/Pure/Isar/keyword.ML
changeset 63429 baedd4724f08
parent 61618 27af754f50ca
child 63430 9c5fcd355a2d
     1.1 --- a/src/Pure/Isar/keyword.ML	Fri Jul 08 22:22:51 2016 +0200
     1.2 +++ b/src/Pure/Isar/keyword.ML	Sun Jul 10 11:18:35 2016 +0200
     1.3 @@ -33,13 +33,14 @@
     1.4    val prf_script_goal: string
     1.5    val prf_script_asm_goal: string
     1.6    type spec = (string * string list) * string list
     1.7 +  val no_spec: spec
     1.8    type keywords
     1.9    val minor_keywords: keywords -> Scan.lexicon
    1.10    val major_keywords: keywords -> Scan.lexicon
    1.11    val no_command_keywords: keywords -> keywords
    1.12    val empty_keywords: keywords
    1.13    val merge_keywords: keywords * keywords -> keywords
    1.14 -  val add_keywords: ((string * Position.T) * spec option) list -> keywords -> keywords
    1.15 +  val add_keywords: ((string * Position.T) * spec) list -> keywords -> keywords
    1.16    val is_keyword: keywords -> string -> bool
    1.17    val is_command: keywords -> string -> bool
    1.18    val is_literal: keywords -> string -> bool
    1.19 @@ -116,6 +117,8 @@
    1.20  
    1.21  type spec = (string * string list) * string list;
    1.22  
    1.23 +val no_spec: spec = (("", []), []);
    1.24 +
    1.25  type entry =
    1.26   {pos: Position.T,
    1.27    id: serial,
    1.28 @@ -131,7 +134,6 @@
    1.29    else {pos = pos, id = serial (), kind = kind, files = files, tags = tags};
    1.30  
    1.31  
    1.32 -
    1.33  (** keyword tables **)
    1.34  
    1.35  (* type keywords *)
    1.36 @@ -168,18 +170,17 @@
    1.37      Symtab.merge (K true) (commands1, commands2));
    1.38  
    1.39  val add_keywords =
    1.40 -  fold (fn ((name, pos), opt_spec) => map_keywords (fn (minor, major, commands) =>
    1.41 -    (case opt_spec of
    1.42 -      NONE =>
    1.43 -        let
    1.44 -          val minor' = Scan.extend_lexicon (Symbol.explode name) minor;
    1.45 -        in (minor', major, commands) end
    1.46 -    | SOME spec =>
    1.47 -        let
    1.48 -          val entry = check_spec pos spec;
    1.49 -          val major' = Scan.extend_lexicon (Symbol.explode name) major;
    1.50 -          val commands' = Symtab.update (name, entry) commands;
    1.51 -        in (minor, major', commands') end)));
    1.52 +  fold (fn ((name, pos), spec as ((kind, _), _)) => map_keywords (fn (minor, major, commands) =>
    1.53 +    if kind = "" then
    1.54 +      let
    1.55 +        val minor' = Scan.extend_lexicon (Symbol.explode name) minor;
    1.56 +      in (minor', major, commands) end
    1.57 +    else
    1.58 +      let
    1.59 +        val entry = check_spec pos spec;
    1.60 +        val major' = Scan.extend_lexicon (Symbol.explode name) major;
    1.61 +        val commands' = Symtab.update (name, entry) commands;
    1.62 +      in (minor, major', commands') end));
    1.63  
    1.64  
    1.65  (* keyword status *)