clarified lazy lexicons within Keywords: measurable speedup of Sessions.deps;
authorwenzelm
Sun Nov 26 13:19:52 2017 +0100 (16 months ago)
changeset 670900ec94bb9cec4
parent 67089 c96ee0eb0d5f
child 67091 1393c2340eec
clarified lazy lexicons within Keywords: measurable speedup of Sessions.deps;
src/Pure/Isar/keyword.scala
     1.1 --- a/src/Pure/Isar/keyword.scala	Sat Nov 25 15:22:17 2017 +0100
     1.2 +++ b/src/Pure/Isar/keyword.scala	Sun Nov 26 13:19:52 2017 +0100
     1.3 @@ -113,8 +113,6 @@
     1.4    }
     1.5  
     1.6    class Keywords private(
     1.7 -    val minor: Scan.Lexicon = Scan.Lexicon.empty,
     1.8 -    val major: Scan.Lexicon = Scan.Lexicon.empty,
     1.9      val kinds: Map[String, String] = Map.empty,
    1.10      val load_commands: Map[String, List[String]] = Map.empty)
    1.11    {
    1.12 @@ -134,14 +132,12 @@
    1.13  
    1.14      /* merge */
    1.15  
    1.16 -    def is_empty: Boolean = minor.is_empty && major.is_empty
    1.17 +    def is_empty: Boolean = kinds.isEmpty
    1.18  
    1.19      def ++ (other: Keywords): Keywords =
    1.20        if (this eq other) this
    1.21        else if (is_empty) other
    1.22        else {
    1.23 -        val minor1 = minor ++ other.minor
    1.24 -        val major1 = major ++ other.major
    1.25          val kinds1 =
    1.26            if (kinds eq other.kinds) kinds
    1.27            else if (kinds.isEmpty) other.kinds
    1.28 @@ -152,7 +148,7 @@
    1.29            else
    1.30              (load_commands /: other.load_commands) {
    1.31                case (m, e) => if (m.isDefinedAt(e._1)) m else m + e }
    1.32 -        new Keywords(minor1, major1, kinds1, load_commands1)
    1.33 +        new Keywords(kinds1, load_commands1)
    1.34        }
    1.35  
    1.36  
    1.37 @@ -161,10 +157,6 @@
    1.38      def + (name: String, kind: String = "", exts: List[String] = Nil): Keywords =
    1.39      {
    1.40        val kinds1 = kinds + (name -> kind)
    1.41 -      val (minor1, major1) =
    1.42 -        if (kind == "" || kind == BEFORE_COMMAND || kind == QUASI_COMMAND)
    1.43 -          (minor + name, major)
    1.44 -        else (minor, major + name)
    1.45        val load_commands1 =
    1.46          if (kind == THY_LOAD) {
    1.47            if (!Symbol.iterator(name).forall(Symbol.is_ascii(_)))
    1.48 @@ -172,7 +164,7 @@
    1.49            load_commands + (name -> exts)
    1.50          }
    1.51          else load_commands
    1.52 -      new Keywords(minor1, major1, kinds1, load_commands1)
    1.53 +      new Keywords(kinds1, load_commands1)
    1.54      }
    1.55  
    1.56      def add_keywords(header: Thy_Header.Keywords): Keywords =
    1.57 @@ -207,5 +199,20 @@
    1.58  
    1.59      def load_commands_in(text: String): Boolean =
    1.60        load_commands.exists({ case (cmd, _) => text.containsSlice(cmd) })
    1.61 +
    1.62 +
    1.63 +    /* lexicons */
    1.64 +
    1.65 +    private def make_lexicon(is_minor: Boolean): Scan.Lexicon =
    1.66 +      (Scan.Lexicon.empty /: kinds)(
    1.67 +        {
    1.68 +          case (lex, (name, kind)) =>
    1.69 +            if ((kind == "" || kind == BEFORE_COMMAND || kind == QUASI_COMMAND) == is_minor)
    1.70 +              lex + name
    1.71 +            else lex
    1.72 +        })
    1.73 +
    1.74 +    lazy val minor: Scan.Lexicon = make_lexicon(true)
    1.75 +    lazy val major: Scan.Lexicon = make_lexicon(false)
    1.76    }
    1.77  }