1.1 --- a/src/Pure/Thy/completion.scala	Wed Jul 06 23:11:59 2011 +0200
     1.2 +++ b/src/Pure/Thy/completion.scala	Thu Jul 07 13:48:30 2011 +0200
     1.3 @@ -62,15 +62,15 @@
     1.4  
     1.5    def + (keyword: String): Completion = this + (keyword, keyword)
     1.6  
     1.7 -  def + (symbols: Symbol.Interpretation): Completion =
     1.8 +  def add_symbols: Completion =
     1.9    {
    1.10      val words =
    1.11 -      (for ((x, _) <- symbols.names) yield (x, x)).toList :::
    1.12 -      (for ((x, y) <- symbols.names) yield (y, x)).toList :::
    1.13 -      (for ((x, y) <- symbols.abbrevs if Completion.is_word(y)) yield (y, x)).toList
    1.14 +      (for ((x, _) <- Symbol.names) yield (x, x)).toList :::
    1.15 +      (for ((x, y) <- Symbol.names) yield (y, x)).toList :::
    1.16 +      (for ((x, y) <- Symbol.abbrevs if Completion.is_word(y)) yield (y, x)).toList
    1.17  
    1.18      val abbrs =
    1.19 -      (for ((x, y) <- symbols.abbrevs if !Completion.is_word(y))
    1.20 +      (for ((x, y) <- Symbol.abbrevs if !Completion.is_word(y))
    1.21          yield (y.reverse.toString, (y, x))).toList
    1.22  
    1.23      val old = this