# HG changeset patch
# User wenzelm
# Date 1330025045 -3600
# Node ID a02115865bcc1b2dad00dcd2ef2ffb4ca44188a5
# Parent  630542c79604b4fc9da7eb054313658322a70a4f
streamlined abstract datatype;

diff -r 630542c79604 -r a02115865bcc src/Pure/Isar/outer_syntax.scala
--- a/src/Pure/Isar/outer_syntax.scala	Thu Feb 23 20:23:19 2012 +0100
+++ b/src/Pure/Isar/outer_syntax.scala	Thu Feb 23 20:24:05 2012 +0100
@@ -33,29 +33,22 @@
     result += '"'
     result.toString
   }
+
+  def init(): Outer_Syntax = new Outer_Syntax()
 }
 
-class Outer_Syntax
+class Outer_Syntax private(
+  keywords: Map[String, String] = Map((";" -> Keyword.DIAG)),
+  lexicon: Scan.Lexicon = Scan.Lexicon.empty,
+  val completion: Completion = Completion.init())
 {
-  protected val keywords: Map[String, String] = Map((";" -> Keyword.DIAG))
-  protected val lexicon: Scan.Lexicon = Scan.Lexicon.empty
-  lazy val completion: Completion = Completion.init()  // FIXME odd initialization
-
   def keyword_kind(name: String): Option[String] = keywords.get(name)
 
   def + (name: String, kind: String, replace: String): Outer_Syntax =
-  {
-    val new_keywords = keywords + (name -> kind)
-    val new_lexicon = lexicon + name
-    val new_completion =
-      if (Keyword.control(kind)) completion
-      else completion + (name, replace)
-    new Outer_Syntax {
-      override val lexicon = new_lexicon
-      override val keywords = new_keywords
-      override lazy val completion = new_completion
-    }
-  }
+    new Outer_Syntax(
+      keywords + (name -> kind),
+      lexicon + name,
+      if (Keyword.control(kind)) completion else completion + (name, replace))
 
   def + (name: String, kind: String): Outer_Syntax = this + (name, kind, name)
 
diff -r 630542c79604 -r a02115865bcc src/Pure/System/session.scala
--- a/src/Pure/System/session.scala	Thu Feb 23 20:23:19 2012 +0100
+++ b/src/Pure/System/session.scala	Thu Feb 23 20:24:05 2012 +0100
@@ -116,7 +116,7 @@
 
   @volatile var verbose: Boolean = false
 
-  @volatile private var syntax = new Outer_Syntax
+  @volatile private var syntax = Outer_Syntax.init()
   def current_syntax(): Outer_Syntax = syntax
 
   @volatile private var reverse_syslog = List[XML.Elem]()