clarified lazy Completion within Outer_Syntax: measurable speedup of Sessions.deps;
authorwenzelm
Sat Nov 04 17:11:21 2017 +0100 (18 months ago)
changeset 67004af72fa58f71b
parent 67003 49850a679c2c
child 67005 11fca474d87a
clarified lazy Completion within Outer_Syntax: measurable speedup of Sessions.deps;
src/Pure/General/completion.scala
src/Pure/Isar/outer_syntax.scala
src/Pure/System/options.scala
src/Pure/Thy/sessions.scala
src/Pure/Thy/thy_header.scala
src/Tools/VSCode/src/document_model.scala
src/Tools/jEdit/src/completion_popup.scala
src/Tools/jEdit/src/isabelle.scala
     1.1 --- a/src/Pure/General/completion.scala	Sat Nov 04 15:24:40 2017 +0100
     1.2 +++ b/src/Pure/General/completion.scala	Sat Nov 04 17:11:21 2017 +0100
     1.3 @@ -253,12 +253,13 @@
     1.4    }
     1.5  
     1.6  
     1.7 -  /* init */
     1.8 +  /* make */
     1.9  
    1.10    val empty: Completion = new Completion()
    1.11  
    1.12 -  lazy val init: Completion =
    1.13 -    empty.add_symbols.add_abbrevs(Completion.symbol_abbrevs ::: Completion.default_abbrevs)
    1.14 +  def make(keywords: List[String], abbrevs: List[(String, String)]): Completion =
    1.15 +    empty.add_symbols.add_keywords(keywords).add_abbrevs(
    1.16 +      Completion.symbol_abbrevs ::: Completion.default_abbrevs ::: abbrevs)
    1.17  
    1.18  
    1.19    /* word parsers */
    1.20 @@ -337,39 +338,12 @@
    1.21  }
    1.22  
    1.23  final class Completion private(
    1.24 -  protected val keywords: Set[String] = Set.empty,
    1.25 -  protected val words_lex: Scan.Lexicon = Scan.Lexicon.empty,
    1.26 -  protected val words_map: Multi_Map[String, String] = Multi_Map.empty,
    1.27 -  protected val abbrevs_lex: Scan.Lexicon = Scan.Lexicon.empty,
    1.28 -  protected val abbrevs_map: Multi_Map[String, (String, String)] = Multi_Map.empty)
    1.29 +  keywords: Set[String] = Set.empty,
    1.30 +  words_lex: Scan.Lexicon = Scan.Lexicon.empty,
    1.31 +  words_map: Multi_Map[String, String] = Multi_Map.empty,
    1.32 +  abbrevs_lex: Scan.Lexicon = Scan.Lexicon.empty,
    1.33 +  abbrevs_map: Multi_Map[String, (String, String)] = Multi_Map.empty)
    1.34  {
    1.35 -  /* merge */
    1.36 -
    1.37 -  def is_empty: Boolean =
    1.38 -    keywords.isEmpty &&
    1.39 -    words_lex.is_empty &&
    1.40 -    words_map.isEmpty &&
    1.41 -    abbrevs_lex.is_empty &&
    1.42 -    abbrevs_map.isEmpty
    1.43 -
    1.44 -  def ++ (other: Completion): Completion =
    1.45 -    if (this eq other) this
    1.46 -    else if (is_empty) other
    1.47 -    else {
    1.48 -      val keywords1 =
    1.49 -        if (keywords eq other.keywords) keywords
    1.50 -        else if (keywords.isEmpty) other.keywords
    1.51 -        else (keywords /: other.keywords) { case (ks, k) => if (ks(k)) ks else ks + k }
    1.52 -      val words_lex1 = words_lex ++ other.words_lex
    1.53 -      val words_map1 = words_map ++ other.words_map
    1.54 -      val abbrevs_lex1 = abbrevs_lex ++ other.abbrevs_lex
    1.55 -      val abbrevs_map1 = abbrevs_map ++ other.abbrevs_map
    1.56 -      if ((keywords eq keywords1) && (words_lex eq words_lex1) && (words_map eq words_map1) &&
    1.57 -        (abbrevs_lex eq abbrevs_lex1) && (abbrevs_map eq abbrevs_map1)) this
    1.58 -      else new Completion(keywords1, words_lex1, words_map1, abbrevs_lex1, abbrevs_map1)
    1.59 -    }
    1.60 -
    1.61 -
    1.62    /* keywords */
    1.63  
    1.64    private def is_symbol(name: String): Boolean = Symbol.names.isDefinedAt(name)
    1.65 @@ -380,6 +354,13 @@
    1.66    def add_keyword(keyword: String): Completion =
    1.67      new Completion(keywords + keyword, words_lex, words_map, abbrevs_lex, abbrevs_map)
    1.68  
    1.69 +  def add_keywords(names: List[String]): Completion =
    1.70 +  {
    1.71 +    val keywords1 = (keywords /: names) { case (ks, k) => if (ks(k)) ks else ks + k }
    1.72 +    if (keywords eq keywords1) this
    1.73 +    else new Completion(keywords1, words_lex, words_map, abbrevs_lex, abbrevs_map)
    1.74 +  }
    1.75 +
    1.76  
    1.77    /* symbols and abbrevs */
    1.78  
     2.1 --- a/src/Pure/Isar/outer_syntax.scala	Sat Nov 04 15:24:40 2017 +0100
     2.2 +++ b/src/Pure/Isar/outer_syntax.scala	Sat Nov 04 17:11:21 2017 +0100
     2.3 @@ -16,8 +16,6 @@
     2.4  
     2.5    val empty: Outer_Syntax = new Outer_Syntax()
     2.6  
     2.7 -  lazy val init: Outer_Syntax = new Outer_Syntax(completion = Completion.init)
     2.8 -
     2.9    def merge(syns: List[Outer_Syntax]): Outer_Syntax = (empty /: syns)(_ ++ _)
    2.10  
    2.11  
    2.12 @@ -47,7 +45,6 @@
    2.13  
    2.14  final class Outer_Syntax private(
    2.15    val keywords: Keyword.Keywords = Keyword.Keywords.empty,
    2.16 -  val completion: Completion = Completion.empty,
    2.17    val rev_abbrevs: Thy_Header.Abbrevs = Nil,
    2.18    val language_context: Completion.Language_Context = Completion.Language_Context.outer,
    2.19    val has_tokens: Boolean = true)
    2.20 @@ -60,16 +57,8 @@
    2.21    /* keywords */
    2.22  
    2.23    def + (name: String, kind: String = "", exts: List[String] = Nil): Outer_Syntax =
    2.24 -  {
    2.25 -    val keywords1 = keywords + (name, kind, exts)
    2.26 -    val completion1 =
    2.27 -      completion.add_keyword(name).
    2.28 -        add_abbrevs(
    2.29 -          (if (Keyword.theory_block.contains(kind)) List((name, name + "\nbegin\n\u0007\nend"))
    2.30 -           else Nil) :::
    2.31 -          (if (Completion.Word_Parsers.is_word(name)) List((name, name)) else Nil))
    2.32 -    new Outer_Syntax(keywords1, completion1, rev_abbrevs, language_context, true)
    2.33 -  }
    2.34 +    new Outer_Syntax(
    2.35 +      keywords + (name, kind, exts), rev_abbrevs, language_context, has_tokens = true)
    2.36  
    2.37    def add_keywords(keywords: Thy_Header.Keywords): Outer_Syntax =
    2.38      (this /: keywords) {
    2.39 @@ -87,17 +76,31 @@
    2.40    def add_abbrevs(new_abbrevs: Thy_Header.Abbrevs): Outer_Syntax =
    2.41      if (new_abbrevs.isEmpty) this
    2.42      else {
    2.43 -      val completion1 =
    2.44 -        completion.add_abbrevs(
    2.45 -          (for ((a, b) <- new_abbrevs) yield {
    2.46 +      val rev_abbrevs1 = Library.distinct(new_abbrevs) reverse_::: rev_abbrevs
    2.47 +      new Outer_Syntax(keywords, rev_abbrevs1, language_context, has_tokens)
    2.48 +    }
    2.49 +
    2.50 +
    2.51 +  /* completion */
    2.52 +
    2.53 +  lazy val completion: Completion =
    2.54 +  {
    2.55 +    val completion_keywords = (keywords.minor.iterator ++ keywords.major.iterator).toList
    2.56 +    val completion_abbrevs =
    2.57 +      completion_keywords.flatMap(name =>
    2.58 +        (if (Keyword.theory_block.contains(keywords.kinds(name)))
    2.59 +          List((name, name + "\nbegin\n\u0007\nend"))
    2.60 +         else Nil) :::
    2.61 +        (if (Completion.Word_Parsers.is_word(name)) List((name, name)) else Nil)) :::
    2.62 +      abbrevs.flatMap(
    2.63 +        { case (a, b) =>
    2.64              val a1 = Symbol.decode(a)
    2.65              val a2 = Symbol.encode(a)
    2.66              val b1 = Symbol.decode(b)
    2.67              List((a1, b1), (a2, b1))
    2.68 -          }).flatten)
    2.69 -      val rev_abbrevs1 = Library.distinct(new_abbrevs) reverse_::: rev_abbrevs
    2.70 -      new Outer_Syntax(keywords, completion1, rev_abbrevs1, language_context, has_tokens)
    2.71 -    }
    2.72 +        })
    2.73 +    Completion.make(completion_keywords, completion_abbrevs)
    2.74 +  }
    2.75  
    2.76  
    2.77    /* build */
    2.78 @@ -110,11 +113,9 @@
    2.79      else if (this eq Outer_Syntax.empty) other
    2.80      else {
    2.81        val keywords1 = keywords ++ other.keywords
    2.82 -      val completion1 = completion ++ other.completion
    2.83        val rev_abbrevs1 = Library.merge(rev_abbrevs, other.rev_abbrevs)
    2.84 -      if ((keywords eq keywords1) && (completion eq completion1) && (rev_abbrevs eq rev_abbrevs1))
    2.85 -        this
    2.86 -      else new Outer_Syntax(keywords1, completion1, rev_abbrevs1, language_context, has_tokens)
    2.87 +      if ((keywords eq keywords1) && (rev_abbrevs eq rev_abbrevs1)) this
    2.88 +      else new Outer_Syntax(keywords1, rev_abbrevs1, language_context, has_tokens)
    2.89      }
    2.90  
    2.91  
    2.92 @@ -127,13 +128,12 @@
    2.93    /* language context */
    2.94  
    2.95    def set_language_context(context: Completion.Language_Context): Outer_Syntax =
    2.96 -    new Outer_Syntax(keywords, completion, rev_abbrevs, context, has_tokens)
    2.97 +    new Outer_Syntax(keywords, rev_abbrevs, context, has_tokens)
    2.98  
    2.99    def no_tokens: Outer_Syntax =
   2.100    {
   2.101      require(keywords.is_empty)
   2.102      new Outer_Syntax(
   2.103 -      completion = completion,
   2.104        rev_abbrevs = rev_abbrevs,
   2.105        language_context = language_context,
   2.106        has_tokens = false)
     3.1 --- a/src/Pure/System/options.scala	Sat Nov 04 15:24:40 2017 +0100
     3.2 +++ b/src/Pure/System/options.scala	Sat Nov 04 17:11:21 2017 +0100
     3.3 @@ -71,13 +71,13 @@
     3.4    private val PREFS_DIR = Path.explode("$ISABELLE_HOME_USER/etc")
     3.5    private val PREFS = PREFS_DIR + Path.basic("preferences")
     3.6  
     3.7 -  lazy val options_syntax =
     3.8 -    Outer_Syntax.init + ":" + "=" + "--" + Symbol.comment + Symbol.comment_decoded +
     3.9 +  val options_syntax =
    3.10 +    Outer_Syntax.empty + ":" + "=" + "--" + Symbol.comment + Symbol.comment_decoded +
    3.11        (SECTION, Keyword.DOCUMENT_HEADING) +
    3.12        (PUBLIC, Keyword.BEFORE_COMMAND) +
    3.13        (OPTION, Keyword.THY_DECL)
    3.14  
    3.15 -  lazy val prefs_syntax = Outer_Syntax.init + "="
    3.16 +  val prefs_syntax = Outer_Syntax.empty + "="
    3.17  
    3.18    trait Parser extends Parse.Parser
    3.19    {
     4.1 --- a/src/Pure/Thy/sessions.scala	Sat Nov 04 15:24:40 2017 +0100
     4.2 +++ b/src/Pure/Thy/sessions.scala	Sat Nov 04 17:11:21 2017 +0100
     4.3 @@ -654,8 +654,8 @@
     4.4    private val GLOBAL = "global"
     4.5    private val DOCUMENT_FILES = "document_files"
     4.6  
     4.7 -  lazy val root_syntax =
     4.8 -    Outer_Syntax.init + "(" + ")" + "+" + "," + "=" + "[" + "]" + GLOBAL + IN +
     4.9 +  val root_syntax =
    4.10 +    Outer_Syntax.empty + "(" + ")" + "+" + "," + "=" + "[" + "]" + GLOBAL + IN +
    4.11        (CHAPTER, Keyword.THY_DECL) +
    4.12        (SESSION, Keyword.THY_DECL) +
    4.13        (DESCRIPTION, Keyword.QUASI_COMMAND) +
     5.1 --- a/src/Pure/Thy/thy_header.scala	Sat Nov 04 15:24:40 2017 +0100
     5.2 +++ b/src/Pure/Thy/thy_header.scala	Sat Nov 04 17:11:21 2017 +0100
     5.3 @@ -65,8 +65,8 @@
     5.4    private val bootstrap_keywords =
     5.5      Keyword.Keywords.empty.add_keywords(bootstrap_header)
     5.6  
     5.7 -  lazy val bootstrap_syntax: Outer_Syntax =
     5.8 -    Outer_Syntax.init.add_keywords(bootstrap_header)
     5.9 +  val bootstrap_syntax: Outer_Syntax =
    5.10 +    Outer_Syntax.empty.add_keywords(bootstrap_header)
    5.11  
    5.12  
    5.13    /* file name vs. theory name */
     6.1 --- a/src/Tools/VSCode/src/document_model.scala	Sat Nov 04 15:24:40 2017 +0100
     6.2 +++ b/src/Tools/VSCode/src/document_model.scala	Sat Nov 04 17:11:21 2017 +0100
     6.3 @@ -240,5 +240,5 @@
     6.4    /* syntax */
     6.5  
     6.6    def syntax(): Outer_Syntax =
     6.7 -    if (is_theory) session.recent_syntax(node_name) else Outer_Syntax.init
     6.8 +    if (is_theory) session.recent_syntax(node_name) else Outer_Syntax.empty
     6.9  }
     7.1 --- a/src/Tools/jEdit/src/completion_popup.scala	Sat Nov 04 15:24:40 2017 +0100
     7.2 +++ b/src/Tools/jEdit/src/completion_popup.scala	Sat Nov 04 17:11:21 2017 +0100
     7.3 @@ -421,7 +421,7 @@
     7.4      name: String = null,
     7.5      instant_popups: Boolean = false,
     7.6      enter_adds_to_history: Boolean = true,
     7.7 -    syntax: Outer_Syntax = Outer_Syntax.init) extends
     7.8 +    syntax: Outer_Syntax = Outer_Syntax.empty) extends
     7.9      HistoryTextField(name, instant_popups, enter_adds_to_history)
    7.10    {
    7.11      text_field =>
     8.1 --- a/src/Tools/jEdit/src/isabelle.scala	Sat Nov 04 15:24:40 2017 +0100
     8.2 +++ b/src/Tools/jEdit/src/isabelle.scala	Sat Nov 04 17:11:21 2017 +0100
     8.3 @@ -37,16 +37,16 @@
     8.4        "isabelle-root",    // session ROOT
     8.5        "sml")              // Standard ML (not Isabelle/ML)
     8.6  
     8.7 -  private lazy val ml_syntax: Outer_Syntax =
     8.8 -    Outer_Syntax.init.no_tokens.
     8.9 +  private val ml_syntax: Outer_Syntax =
    8.10 +    Outer_Syntax.empty.no_tokens.
    8.11        set_language_context(Completion.Language_Context.ML_outer)
    8.12  
    8.13 -  private lazy val sml_syntax: Outer_Syntax =
    8.14 -    Outer_Syntax.init.no_tokens.
    8.15 +  private val sml_syntax: Outer_Syntax =
    8.16 +    Outer_Syntax.empty.no_tokens.
    8.17        set_language_context(Completion.Language_Context.SML_outer)
    8.18  
    8.19 -  private lazy val news_syntax: Outer_Syntax =
    8.20 -    Outer_Syntax.init.no_tokens
    8.21 +  private val news_syntax: Outer_Syntax =
    8.22 +    Outer_Syntax.empty.no_tokens
    8.23  
    8.24    def mode_syntax(mode: String): Option[Outer_Syntax] =
    8.25      mode match {