init only once (see also c0f776b661fa);
authorwenzelm
Wed, 01 Nov 2017 21:02:16 +0100
changeset 66984 a1d3e5df0c95
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
--- a/src/Pure/General/completion.scala	Wed Nov 01 20:46:23 2017 +0100
+++ b/src/Pure/General/completion.scala	Wed Nov 01 21:02:16 2017 +0100
@@ -256,7 +256,8 @@
   /* init */
 
   val empty: Completion = new Completion()
-  def init(): Completion =
+
+  lazy val init: Completion =
     empty.add_symbols.add_abbrevs(Completion.symbol_abbrevs ::: Completion.default_abbrevs)
 
 
--- a/src/Pure/Isar/outer_syntax.scala	Wed Nov 01 20:46:23 2017 +0100
+++ b/src/Pure/Isar/outer_syntax.scala	Wed Nov 01 21:02:16 2017 +0100
@@ -16,7 +16,7 @@
 
   val empty: Outer_Syntax = new Outer_Syntax()
 
-  def init(): Outer_Syntax = new Outer_Syntax(completion = Completion.init())
+  lazy val init: Outer_Syntax = new Outer_Syntax(completion = Completion.init)
 
   def merge(syns: List[Outer_Syntax]): Outer_Syntax = (empty /: syns)(_ ++ _)
 
--- a/src/Pure/System/options.scala	Wed Nov 01 20:46:23 2017 +0100
+++ b/src/Pure/System/options.scala	Wed Nov 01 21:02:16 2017 +0100
@@ -72,12 +72,12 @@
   private val PREFS = PREFS_DIR + Path.basic("preferences")
 
   lazy val options_syntax =
-    Outer_Syntax.init() + ":" + "=" + "--" + Symbol.comment + Symbol.comment_decoded +
+    Outer_Syntax.init + ":" + "=" + "--" + Symbol.comment + Symbol.comment_decoded +
       (SECTION, Keyword.DOCUMENT_HEADING) +
       (PUBLIC, Keyword.BEFORE_COMMAND) +
       (OPTION, Keyword.THY_DECL)
 
-  lazy val prefs_syntax = Outer_Syntax.init() + "="
+  lazy val prefs_syntax = Outer_Syntax.init + "="
 
   trait Parser extends Parse.Parser
   {
--- a/src/Pure/Thy/sessions.scala	Wed Nov 01 20:46:23 2017 +0100
+++ b/src/Pure/Thy/sessions.scala	Wed Nov 01 21:02:16 2017 +0100
@@ -638,7 +638,7 @@
   private val DOCUMENT_FILES = "document_files"
 
   lazy val root_syntax =
-    Outer_Syntax.init() + "(" + ")" + "+" + "," + "=" + "[" + "]" + GLOBAL + IN +
+    Outer_Syntax.init + "(" + ")" + "+" + "," + "=" + "[" + "]" + GLOBAL + IN +
       (CHAPTER, Keyword.THY_DECL) +
       (SESSION, Keyword.THY_DECL) +
       (DESCRIPTION, Keyword.QUASI_COMMAND) +
--- a/src/Pure/Thy/thy_header.scala	Wed Nov 01 20:46:23 2017 +0100
+++ b/src/Pure/Thy/thy_header.scala	Wed Nov 01 21:02:16 2017 +0100
@@ -66,7 +66,7 @@
     Keyword.Keywords.empty.add_keywords(bootstrap_header)
 
   lazy val bootstrap_syntax: Outer_Syntax =
-    Outer_Syntax.init().add_keywords(bootstrap_header)
+    Outer_Syntax.init.add_keywords(bootstrap_header)
 
 
   /* file name vs. theory name */
--- a/src/Tools/VSCode/src/document_model.scala	Wed Nov 01 20:46:23 2017 +0100
+++ b/src/Tools/VSCode/src/document_model.scala	Wed Nov 01 21:02:16 2017 +0100
@@ -239,8 +239,6 @@
 
   /* syntax */
 
-  lazy private val syntax0 = Outer_Syntax.init()
-
   def syntax(): Outer_Syntax =
-    if (is_theory) session.recent_syntax(node_name) else syntax0
+    if (is_theory) session.recent_syntax(node_name) else Outer_Syntax.init
 }
--- a/src/Tools/jEdit/src/isabelle.scala	Wed Nov 01 20:46:23 2017 +0100
+++ b/src/Tools/jEdit/src/isabelle.scala	Wed Nov 01 21:02:16 2017 +0100
@@ -38,15 +38,15 @@
       "sml")              // Standard ML (not Isabelle/ML)
 
   private lazy val ml_syntax: Outer_Syntax =
-    Outer_Syntax.init().no_tokens.
+    Outer_Syntax.init.no_tokens.
       set_language_context(Completion.Language_Context.ML_outer)
 
   private lazy val sml_syntax: Outer_Syntax =
-    Outer_Syntax.init().no_tokens.
+    Outer_Syntax.init.no_tokens.
       set_language_context(Completion.Language_Context.SML_outer)
 
   private lazy val news_syntax: Outer_Syntax =
-    Outer_Syntax.init().no_tokens
+    Outer_Syntax.init.no_tokens
 
   def mode_syntax(mode: String): Option[Outer_Syntax] =
     mode match {