src/Pure/Isar/outer_syntax.scala
changeset 46626 a02115865bcc
parent 46624 dc4c72092088
child 46712 8650d9a95736
     1.1 --- a/src/Pure/Isar/outer_syntax.scala	Thu Feb 23 20:23:19 2012 +0100
     1.2 +++ b/src/Pure/Isar/outer_syntax.scala	Thu Feb 23 20:24:05 2012 +0100
     1.3 @@ -33,29 +33,22 @@
     1.4      result += '"'
     1.5      result.toString
     1.6    }
     1.7 +
     1.8 +  def init(): Outer_Syntax = new Outer_Syntax()
     1.9  }
    1.10  
    1.11 -class Outer_Syntax
    1.12 +class Outer_Syntax private(
    1.13 +  keywords: Map[String, String] = Map((";" -> Keyword.DIAG)),
    1.14 +  lexicon: Scan.Lexicon = Scan.Lexicon.empty,
    1.15 +  val completion: Completion = Completion.init())
    1.16  {
    1.17 -  protected val keywords: Map[String, String] = Map((";" -> Keyword.DIAG))
    1.18 -  protected val lexicon: Scan.Lexicon = Scan.Lexicon.empty
    1.19 -  lazy val completion: Completion = Completion.init()  // FIXME odd initialization
    1.20 -
    1.21    def keyword_kind(name: String): Option[String] = keywords.get(name)
    1.22  
    1.23    def + (name: String, kind: String, replace: String): Outer_Syntax =
    1.24 -  {
    1.25 -    val new_keywords = keywords + (name -> kind)
    1.26 -    val new_lexicon = lexicon + name
    1.27 -    val new_completion =
    1.28 -      if (Keyword.control(kind)) completion
    1.29 -      else completion + (name, replace)
    1.30 -    new Outer_Syntax {
    1.31 -      override val lexicon = new_lexicon
    1.32 -      override val keywords = new_keywords
    1.33 -      override lazy val completion = new_completion
    1.34 -    }
    1.35 -  }
    1.36 +    new Outer_Syntax(
    1.37 +      keywords + (name -> kind),
    1.38 +      lexicon + name,
    1.39 +      if (Keyword.control(kind)) completion else completion + (name, replace))
    1.40  
    1.41    def + (name: String, kind: String): Outer_Syntax = this + (name, kind, name)
    1.42