init only once (see also c0f776b661fa);
authorwenzelm
Wed Nov 01 21:02:16 2017 +0100 (18 months ago)
changeset 66984a1d3e5df0c95
parent 66983 df83b66f1d94
child 66985 7382ff5b46b9
init only once (see also c0f776b661fa);
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/isabelle.scala
     1.1 --- a/src/Pure/General/completion.scala	Wed Nov 01 20:46:23 2017 +0100
     1.2 +++ b/src/Pure/General/completion.scala	Wed Nov 01 21:02:16 2017 +0100
     1.3 @@ -256,7 +256,8 @@
     1.4    /* init */
     1.5  
     1.6    val empty: Completion = new Completion()
     1.7 -  def init(): Completion =
     1.8 +
     1.9 +  lazy val init: Completion =
    1.10      empty.add_symbols.add_abbrevs(Completion.symbol_abbrevs ::: Completion.default_abbrevs)
    1.11  
    1.12  
     2.1 --- a/src/Pure/Isar/outer_syntax.scala	Wed Nov 01 20:46:23 2017 +0100
     2.2 +++ b/src/Pure/Isar/outer_syntax.scala	Wed Nov 01 21:02:16 2017 +0100
     2.3 @@ -16,7 +16,7 @@
     2.4  
     2.5    val empty: Outer_Syntax = new Outer_Syntax()
     2.6  
     2.7 -  def init(): Outer_Syntax = new Outer_Syntax(completion = Completion.init())
     2.8 +  lazy val init: Outer_Syntax = new Outer_Syntax(completion = Completion.init)
     2.9  
    2.10    def merge(syns: List[Outer_Syntax]): Outer_Syntax = (empty /: syns)(_ ++ _)
    2.11  
     3.1 --- a/src/Pure/System/options.scala	Wed Nov 01 20:46:23 2017 +0100
     3.2 +++ b/src/Pure/System/options.scala	Wed Nov 01 21:02:16 2017 +0100
     3.3 @@ -72,12 +72,12 @@
     3.4    private val PREFS = PREFS_DIR + Path.basic("preferences")
     3.5  
     3.6    lazy val options_syntax =
     3.7 -    Outer_Syntax.init() + ":" + "=" + "--" + Symbol.comment + Symbol.comment_decoded +
     3.8 +    Outer_Syntax.init + ":" + "=" + "--" + Symbol.comment + Symbol.comment_decoded +
     3.9        (SECTION, Keyword.DOCUMENT_HEADING) +
    3.10        (PUBLIC, Keyword.BEFORE_COMMAND) +
    3.11        (OPTION, Keyword.THY_DECL)
    3.12  
    3.13 -  lazy val prefs_syntax = Outer_Syntax.init() + "="
    3.14 +  lazy val prefs_syntax = Outer_Syntax.init + "="
    3.15  
    3.16    trait Parser extends Parse.Parser
    3.17    {
     4.1 --- a/src/Pure/Thy/sessions.scala	Wed Nov 01 20:46:23 2017 +0100
     4.2 +++ b/src/Pure/Thy/sessions.scala	Wed Nov 01 21:02:16 2017 +0100
     4.3 @@ -638,7 +638,7 @@
     4.4    private val DOCUMENT_FILES = "document_files"
     4.5  
     4.6    lazy val root_syntax =
     4.7 -    Outer_Syntax.init() + "(" + ")" + "+" + "," + "=" + "[" + "]" + GLOBAL + IN +
     4.8 +    Outer_Syntax.init + "(" + ")" + "+" + "," + "=" + "[" + "]" + GLOBAL + IN +
     4.9        (CHAPTER, Keyword.THY_DECL) +
    4.10        (SESSION, Keyword.THY_DECL) +
    4.11        (DESCRIPTION, Keyword.QUASI_COMMAND) +
     5.1 --- a/src/Pure/Thy/thy_header.scala	Wed Nov 01 20:46:23 2017 +0100
     5.2 +++ b/src/Pure/Thy/thy_header.scala	Wed Nov 01 21:02:16 2017 +0100
     5.3 @@ -66,7 +66,7 @@
     5.4      Keyword.Keywords.empty.add_keywords(bootstrap_header)
     5.5  
     5.6    lazy val bootstrap_syntax: Outer_Syntax =
     5.7 -    Outer_Syntax.init().add_keywords(bootstrap_header)
     5.8 +    Outer_Syntax.init.add_keywords(bootstrap_header)
     5.9  
    5.10  
    5.11    /* file name vs. theory name */
     6.1 --- a/src/Tools/VSCode/src/document_model.scala	Wed Nov 01 20:46:23 2017 +0100
     6.2 +++ b/src/Tools/VSCode/src/document_model.scala	Wed Nov 01 21:02:16 2017 +0100
     6.3 @@ -239,8 +239,6 @@
     6.4  
     6.5    /* syntax */
     6.6  
     6.7 -  lazy private val syntax0 = Outer_Syntax.init()
     6.8 -
     6.9    def syntax(): Outer_Syntax =
    6.10 -    if (is_theory) session.recent_syntax(node_name) else syntax0
    6.11 +    if (is_theory) session.recent_syntax(node_name) else Outer_Syntax.init
    6.12  }
     7.1 --- a/src/Tools/jEdit/src/isabelle.scala	Wed Nov 01 20:46:23 2017 +0100
     7.2 +++ b/src/Tools/jEdit/src/isabelle.scala	Wed Nov 01 21:02:16 2017 +0100
     7.3 @@ -38,15 +38,15 @@
     7.4        "sml")              // Standard ML (not Isabelle/ML)
     7.5  
     7.6    private lazy val ml_syntax: Outer_Syntax =
     7.7 -    Outer_Syntax.init().no_tokens.
     7.8 +    Outer_Syntax.init.no_tokens.
     7.9        set_language_context(Completion.Language_Context.ML_outer)
    7.10  
    7.11    private lazy val sml_syntax: Outer_Syntax =
    7.12 -    Outer_Syntax.init().no_tokens.
    7.13 +    Outer_Syntax.init.no_tokens.
    7.14        set_language_context(Completion.Language_Context.SML_outer)
    7.15  
    7.16    private lazy val news_syntax: Outer_Syntax =
    7.17 -    Outer_Syntax.init().no_tokens
    7.18 +    Outer_Syntax.init.no_tokens
    7.19  
    7.20    def mode_syntax(mode: String): Option[Outer_Syntax] =
    7.21      mode match {