changeset 34135 | 63dd95e3b393 |
parent 34097 | 9274a44358c4 |
child 34141 | 297b2149077d |
--- a/src/Pure/Thy/completion.scala Sat Dec 19 11:45:14 2009 +0100 +++ b/src/Pure/Thy/completion.scala Sat Dec 19 11:48:11 2009 +0100 @@ -114,7 +114,7 @@ def complete(line: CharSequence): Option[(String, List[String])] = { abbrevs_lex.parse(abbrevs_lex.keyword, new Completion.Reverse(line)) match { - case abbrevs_lex.Success(rev_a, _) => + case abbrevs_lex.Success((rev_a, _), _) => val (word, c) = abbrevs_map(rev_a) if (word == c) None else Some(word, List(c))