# HG changeset patch # User wenzelm # Date 1511698792 -3600 # Node ID 0ec94bb9cec4e68c4c6c6be0fd861f19cf39e5ec # Parent c96ee0eb0d5f1b365e766976691917d2370c6af1 clarified lazy lexicons within Keywords: measurable speedup of Sessions.deps; diff -r c96ee0eb0d5f -r 0ec94bb9cec4 src/Pure/Isar/keyword.scala --- a/src/Pure/Isar/keyword.scala Sat Nov 25 15:22:17 2017 +0100 +++ b/src/Pure/Isar/keyword.scala Sun Nov 26 13:19:52 2017 +0100 @@ -113,8 +113,6 @@ } class Keywords private( - val minor: Scan.Lexicon = Scan.Lexicon.empty, - val major: Scan.Lexicon = Scan.Lexicon.empty, val kinds: Map[String, String] = Map.empty, val load_commands: Map[String, List[String]] = Map.empty) { @@ -134,14 +132,12 @@ /* merge */ - def is_empty: Boolean = minor.is_empty && major.is_empty + def is_empty: Boolean = kinds.isEmpty def ++ (other: Keywords): Keywords = if (this eq other) this else if (is_empty) other else { - val minor1 = minor ++ other.minor - val major1 = major ++ other.major val kinds1 = if (kinds eq other.kinds) kinds else if (kinds.isEmpty) other.kinds @@ -152,7 +148,7 @@ else (load_commands /: other.load_commands) { case (m, e) => if (m.isDefinedAt(e._1)) m else m + e } - new Keywords(minor1, major1, kinds1, load_commands1) + new Keywords(kinds1, load_commands1) } @@ -161,10 +157,6 @@ def + (name: String, kind: String = "", exts: List[String] = Nil): Keywords = { val kinds1 = kinds + (name -> kind) - val (minor1, major1) = - if (kind == "" || kind == BEFORE_COMMAND || kind == QUASI_COMMAND) - (minor + name, major) - else (minor, major + name) val load_commands1 = if (kind == THY_LOAD) { if (!Symbol.iterator(name).forall(Symbol.is_ascii(_))) @@ -172,7 +164,7 @@ load_commands + (name -> exts) } else load_commands - new Keywords(minor1, major1, kinds1, load_commands1) + new Keywords(kinds1, load_commands1) } def add_keywords(header: Thy_Header.Keywords): Keywords = @@ -207,5 +199,20 @@ def load_commands_in(text: String): Boolean = load_commands.exists({ case (cmd, _) => text.containsSlice(cmd) }) + + + /* lexicons */ + + private def make_lexicon(is_minor: Boolean): Scan.Lexicon = + (Scan.Lexicon.empty /: kinds)( + { + case (lex, (name, kind)) => + if ((kind == "" || kind == BEFORE_COMMAND || kind == QUASI_COMMAND) == is_minor) + lex + name + else lex + }) + + lazy val minor: Scan.Lexicon = make_lexicon(true) + lazy val major: Scan.Lexicon = make_lexicon(false) } }