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