1.1 --- a/src/Pure/Thy/completion.scala	Tue Jun 23 17:43:51 2009 +0200
     1.2 +++ b/src/Pure/Thy/completion.scala	Tue Jun 23 20:09:56 2009 +0200
     1.3 @@ -49,18 +49,19 @@
     1.4    {
     1.5      override val whiteSpace = "".r
     1.6  
     1.7 -    def rev_symb: Parser[String] = """>?[A-Za-z0-9_']+<\\""".r
     1.8 +    def rev_symbol: Parser[String] = """>[A-Za-z0-9_']+<\\""".r
     1.9 +    def rev_symb: Parser[String] = """[A-Za-z0-9_']{2,}<\\""".r
    1.10      def word: Parser[String] = "[a-zA-Z0-9_']{3,}".r
    1.11  
    1.12      def read(in: CharSequence): Option[String] =
    1.13      {
    1.14 -      parse((rev_symb | word) ^^ (_.reverse), new Reverse(in)) match {
    1.15 +      val rev_in = new Reverse(in)
    1.16 +      parse((rev_symbol | rev_symb | word) ^^ (_.reverse), rev_in) match {
    1.17          case Success(result, _) => Some(result)
    1.18          case _ => None
    1.19        }
    1.20      }
    1.21    }
    1.22 -
    1.23  }
    1.24  
    1.25  class Completion
    1.26 @@ -96,12 +97,12 @@
    1.27  
    1.28      val abbrs =
    1.29        (for ((x, y) <- symbols.abbrevs if !Completion.is_word(y))
    1.30 -        yield (y.reverse.toString, (y, symbols.decode(x)))).toList
    1.31 +        yield (y.reverse.toString, (y, x))).toList
    1.32  
    1.33      val old = this
    1.34      new Completion {
    1.35        override val words_lex = old.words_lex ++ words.map(_._1)
    1.36 -      override val words_map = old.words_map ++ words.map(p => (p._1, symbols.decode(p._2)))
    1.37 +      override val words_map = old.words_map ++ words
    1.38        override val abbrevs_lex = old.abbrevs_lex ++ abbrs.map(_._1)
    1.39        override val abbrevs_map = old.abbrevs_map ++ abbrs
    1.40      }
    1.41 @@ -110,21 +111,21 @@
    1.42  
    1.43    /* complete */
    1.44  
    1.45 -  def complete(line: CharSequence): List[(String, String)] =
    1.46 +  def complete(line: CharSequence): Option[(String, List[String])] =
    1.47    {
    1.48 -    val abbrs =
    1.49 -      abbrevs_lex.parse(abbrevs_lex.keyword, new Completion.Reverse(line)) match {
    1.50 -        case abbrevs_lex.Success(rev_a, _) => List(abbrevs_map(rev_a))
    1.51 -        case _ => Nil
    1.52 -      }
    1.53 -
    1.54 -    val compls =
    1.55 -      Completion.Parse.read(line) match {
    1.56 -        case Some(word) => words_lex.completions(word).map(w => (word, words_map(w)))
    1.57 -        case _ => Nil
    1.58 -      }
    1.59 -
    1.60 -    (abbrs ::: compls).sort((p1, p2) => Completion.length_ord(p1._2, p2._2))
    1.61 +    abbrevs_lex.parse(abbrevs_lex.keyword, new Completion.Reverse(line)) match {
    1.62 +      case abbrevs_lex.Success(rev_a, _) =>
    1.63 +        val (word, c) = abbrevs_map(rev_a)
    1.64 +        Some(word, List(c))
    1.65 +      case _ =>
    1.66 +        Completion.Parse.read(line) match {
    1.67 +          case Some(word) =>
    1.68 +            words_lex.completions(word) match {
    1.69 +              case Nil => None
    1.70 +              case cs => Some(word, cs.map(words_map(_)).sort(Completion.length_ord _))
    1.71 +            }
    1.72 +          case None => None
    1.73 +        }
    1.74 +    }
    1.75    }
    1.76 -
    1.77  }