--- 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 {