# HG changeset patch # User wenzelm # Date 1415218875 -3600 # Node ID 29788e989d6188251baf6b28db5f476e23917f92 # Parent 55160ef37e8f723dd1b33a62f6d8eaffe57c3d2a tuned; diff -r 55160ef37e8f -r 29788e989d61 src/Pure/Isar/keyword.ML --- a/src/Pure/Isar/keyword.ML Wed Nov 05 21:10:38 2014 +0100 +++ b/src/Pure/Isar/keyword.ML Wed Nov 05 21:21:15 2014 +0100 @@ -158,28 +158,28 @@ datatype keywords = Keywords of {minor: Scan.lexicon, major: Scan.lexicon, - command_kinds: T Symtab.table}; + commands: T Symtab.table}; fun minor_keywords (Keywords {minor, ...}) = minor; fun major_keywords (Keywords {major, ...}) = major; -fun command_kinds (Keywords {command_kinds, ...}) = command_kinds; +fun commands (Keywords {commands, ...}) = commands; -fun make_keywords (minor, major, command_kinds) = - Keywords {minor = minor, major = major, command_kinds = command_kinds}; +fun make_keywords (minor, major, commands) = + Keywords {minor = minor, major = major, commands = commands}; -fun map_keywords f (Keywords {minor, major, command_kinds}) = - make_keywords (f (minor, major, command_kinds)); +fun map_keywords f (Keywords {minor, major, commands}) = + make_keywords (f (minor, major, commands)); val empty_keywords = make_keywords (Scan.empty_lexicon, Scan.empty_lexicon, Symtab.empty); fun merge_keywords - (Keywords {minor = minor1, major = major1, command_kinds = command_kinds1}, - Keywords {minor = minor2, major = major2, command_kinds = command_kinds2}) = + (Keywords {minor = minor1, major = major1, commands = commands1}, + Keywords {minor = minor2, major = major2, commands = commands2}) = make_keywords (Scan.merge_lexicons (minor1, minor2), Scan.merge_lexicons (major1, major2), - Symtab.merge (K true) (command_kinds1, command_kinds2)); + Symtab.merge (K true) (commands1, commands2)); val no_command_keywords = map_keywords (fn (minor, _, _) => (minor, Scan.empty_lexicon, Symtab.empty)); @@ -187,17 +187,17 @@ (* add keywords *) -fun add (name, opt_kind) = map_keywords (fn (minor, major, command_kinds) => +fun add (name, opt_kind) = map_keywords (fn (minor, major, commands) => (case opt_kind of NONE => let val minor' = Scan.extend_lexicon (Symbol.explode name) minor; - in (minor', major, command_kinds) end + in (minor', major, commands) end | SOME kind => let val major' = Scan.extend_lexicon (Symbol.explode name) major; - val command_kinds' = Symtab.update (name, kind) command_kinds; - in (minor, major', command_kinds') end)); + val commands' = Symtab.update (name, kind) commands; + in (minor, major', commands') end)); (* global state *) @@ -213,7 +213,7 @@ let val keywords = get_keywords () in (minor_keywords keywords, major_keywords keywords) end; -fun get_commands () = command_kinds (get_keywords ()); +fun get_commands () = commands (get_keywords ()); (* lookup *) diff -r 55160ef37e8f -r 29788e989d61 src/Pure/Isar/keyword.scala --- a/src/Pure/Isar/keyword.scala Wed Nov 05 21:10:38 2014 +0100 +++ b/src/Pure/Isar/keyword.scala Wed Nov 05 21:21:15 2014 +0100 @@ -79,7 +79,7 @@ class Keywords private( val minor: Scan.Lexicon = Scan.Lexicon.empty, val major: Scan.Lexicon = Scan.Lexicon.empty, - command_kinds: Map[String, (String, List[String])] = Map.empty) + commands: Map[String, (String, List[String])] = Map.empty) { /* content */ @@ -87,32 +87,32 @@ override def toString: String = { - val keywords = minor.iterator.map(quote(_)).toList - val commands = - for ((name, (kind, files)) <- command_kinds.toList.sortBy(_._1)) yield { + val keywords1 = minor.iterator.map(quote(_)).toList + val keywords2 = + for ((name, (kind, files)) <- commands.toList.sortBy(_._1)) yield { quote(name) + " :: " + quote(kind) + (if (files.isEmpty) "" else " (" + commas_quote(files) + ")") } - (keywords ::: commands).mkString("keywords\n ", " and\n ", "") + (keywords1 ::: keywords2).mkString("keywords\n ", " and\n ", "") } /* add keywords */ def + (name: String): Keywords = - new Keywords(minor + name, major, command_kinds) + new Keywords(minor + name, major, commands) def + (name: String, kind: (String, List[String])): Keywords = { val major1 = major + name - val command_kinds1 = command_kinds + (name -> kind) - new Keywords(minor, major1, command_kinds1) + val commands1 = commands + (name -> kind) + new Keywords(minor, major1, commands1) } /* command kind */ - def command_kind(name: String): Option[String] = command_kinds.get(name).map(_._1) + def command_kind(name: String): Option[String] = commands.get(name).map(_._1) def is_command_kind(token: Token, pred: String => Boolean): Boolean = token.is_command && @@ -122,13 +122,13 @@ /* load commands */ def load_command(name: String): Option[List[String]] = - command_kinds.get(name) match { + commands.get(name) match { case Some((THY_LOAD, exts)) => Some(exts) case _ => None } private lazy val load_commands: List[(String, List[String])] = - (for ((name, (THY_LOAD, files)) <- command_kinds.iterator) yield (name, files)).toList + (for ((name, (THY_LOAD, files)) <- commands.iterator) yield (name, files)).toList def load_commands_in(text: String): Boolean = load_commands.exists({ case (cmd, _) => text.containsSlice(cmd) })