# HG changeset patch
# User wenzelm
# Date 1509566536 -3600
# Node ID a1d3e5df0c95266b879256f7ab1165b40f52b87d
# Parent  df83b66f1d9467da9d4e930430740c97ad858264
init only once (see also c0f776b661fa);

diff -r df83b66f1d94 -r a1d3e5df0c95 src/Pure/General/completion.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)
 
 
diff -r df83b66f1d94 -r a1d3e5df0c95 src/Pure/Isar/outer_syntax.scala
--- 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)(_ ++ _)
 
diff -r df83b66f1d94 -r a1d3e5df0c95 src/Pure/System/options.scala
--- 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
   {
diff -r df83b66f1d94 -r a1d3e5df0c95 src/Pure/Thy/sessions.scala
--- 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) +
diff -r df83b66f1d94 -r a1d3e5df0c95 src/Pure/Thy/thy_header.scala
--- 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 */
diff -r df83b66f1d94 -r a1d3e5df0c95 src/Tools/VSCode/src/document_model.scala
--- 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
 }
diff -r df83b66f1d94 -r a1d3e5df0c95 src/Tools/jEdit/src/isabelle.scala
--- 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 {