1.1 --- a/src/Pure/Thy/completion.scala	Sat Dec 19 11:45:14 2009 +0100
     1.2 +++ b/src/Pure/Thy/completion.scala	Sat Dec 19 11:48:11 2009 +0100
     1.3 @@ -114,7 +114,7 @@
     1.4    def complete(line: CharSequence): Option[(String, List[String])] =
     1.5    {
     1.6      abbrevs_lex.parse(abbrevs_lex.keyword, new Completion.Reverse(line)) match {
     1.7 -      case abbrevs_lex.Success(rev_a, _) =>
     1.8 +      case abbrevs_lex.Success((rev_a, _), _) =>
     1.9          val (word, c) = abbrevs_map(rev_a)
    1.10          if (word == c) None
    1.11          else Some(word, List(c))