# HG changeset patch
# User wenzelm
# Date 1245780596 -7200
# Node ID a5fdf7a76f9d068c8d06cc838b6649f35f5dd7cb
# Parent  e767fee21b22f12245f6d3df50435ec0fc2f9cbc
tuned input: require longer symbol prefix;
clarified result: no decode yet, single word with several completions;

diff -r e767fee21b22 -r a5fdf7a76f9d src/Pure/Thy/completion.scala
--- a/src/Pure/Thy/completion.scala	Tue Jun 23 17:43:51 2009 +0200
+++ b/src/Pure/Thy/completion.scala	Tue Jun 23 20:09:56 2009 +0200
@@ -49,18 +49,19 @@
   {
     override val whiteSpace = "".r
 
-    def rev_symb: Parser[String] = """>?[A-Za-z0-9_']+<\\""".r
+    def rev_symbol: Parser[String] = """>[A-Za-z0-9_']+<\\""".r
+    def rev_symb: Parser[String] = """[A-Za-z0-9_']{2,}<\\""".r
     def word: Parser[String] = "[a-zA-Z0-9_']{3,}".r
 
     def read(in: CharSequence): Option[String] =
     {
-      parse((rev_symb | word) ^^ (_.reverse), new Reverse(in)) match {
+      val rev_in = new Reverse(in)
+      parse((rev_symbol | rev_symb | word) ^^ (_.reverse), rev_in) match {
         case Success(result, _) => Some(result)
         case _ => None
       }
     }
   }
-
 }
 
 class Completion
@@ -96,12 +97,12 @@
 
     val abbrs =
       (for ((x, y) <- symbols.abbrevs if !Completion.is_word(y))
-        yield (y.reverse.toString, (y, symbols.decode(x)))).toList
+        yield (y.reverse.toString, (y, x))).toList
 
     val old = this
     new Completion {
       override val words_lex = old.words_lex ++ words.map(_._1)
-      override val words_map = old.words_map ++ words.map(p => (p._1, symbols.decode(p._2)))
+      override val words_map = old.words_map ++ words
       override val abbrevs_lex = old.abbrevs_lex ++ abbrs.map(_._1)
       override val abbrevs_map = old.abbrevs_map ++ abbrs
     }
@@ -110,21 +111,21 @@
 
   /* complete */
 
-  def complete(line: CharSequence): List[(String, String)] =
+  def complete(line: CharSequence): Option[(String, List[String])] =
   {
-    val abbrs =
-      abbrevs_lex.parse(abbrevs_lex.keyword, new Completion.Reverse(line)) match {
-        case abbrevs_lex.Success(rev_a, _) => List(abbrevs_map(rev_a))
-        case _ => Nil
-      }
-
-    val compls =
-      Completion.Parse.read(line) match {
-        case Some(word) => words_lex.completions(word).map(w => (word, words_map(w)))
-        case _ => Nil
-      }
-
-    (abbrs ::: compls).sort((p1, p2) => Completion.length_ord(p1._2, p2._2))
+    abbrevs_lex.parse(abbrevs_lex.keyword, new Completion.Reverse(line)) match {
+      case abbrevs_lex.Success(rev_a, _) =>
+        val (word, c) = abbrevs_map(rev_a)
+        Some(word, List(c))
+      case _ =>
+        Completion.Parse.read(line) match {
+          case Some(word) =>
+            words_lex.completions(word) match {
+              case Nil => None
+              case cs => Some(word, cs.map(words_map(_)).sort(Completion.length_ord _))
+            }
+          case None => None
+        }
+    }
   }
-
 }