# HG changeset patch
# User wenzelm
# Date 1261492262 -3600
# Node ID ebacba221e3123f84823a3dcc6f3de19acbfb54e
# Parent  903092d615192abb6b6fab31446ca169baa5a5f3
added completion -- lazy avoids excessive table building;
tuned signature;

diff -r 903092d61519 -r ebacba221e31 src/Pure/Isar/outer_keyword.scala
--- a/src/Pure/Isar/outer_keyword.scala	Tue Dec 22 15:00:43 2009 +0100
+++ b/src/Pure/Isar/outer_keyword.scala	Tue Dec 22 15:31:02 2009 +0100
@@ -51,20 +51,23 @@
 
 class Outer_Keyword(symbols: Symbol.Interpretation)
 {
+  protected val keywords: Map[String, String] = Map((";" -> Outer_Keyword.DIAG))
   protected val lexicon: Scan.Lexicon = Scan.Lexicon.empty
-  protected val keywords: Map[String, String] = Map((";" -> Outer_Keyword.DIAG))
+  lazy val completion: Completion = new Completion + symbols
 
-  def keyword(name: String, kind: String): Outer_Keyword =
+  def + (name: String, kind: String): Outer_Keyword =
   {
+    val new_keywords = keywords + (name -> kind)
     val new_lexicon = lexicon + name
-    val new_keywords = keywords + (name -> kind)
+    val new_completion = completion + name
     new Outer_Keyword(symbols) {
       override val lexicon = new_lexicon
       override val keywords = new_keywords
+      override lazy val completion = new_completion
     }
   }
 
-  def keyword(name: String): Outer_Keyword = keyword(name, Outer_Keyword.MINOR)
+  def + (name: String): Outer_Keyword = this + (name, Outer_Keyword.MINOR)
 
   def is_command(name: String): Boolean =
     keywords.get(name) match {