src/Pure/Thy/completion.scala
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))