src/Pure/General/completion.scala
changeset 55687 78c83cd477c1
parent 55674 8a213ab0e78a
child 55692 19e8b00684f7
--- a/src/Pure/General/completion.scala	Sun Feb 23 10:44:57 2014 +0100
+++ b/src/Pure/General/completion.scala	Sun Feb 23 14:39:51 2014 +0100
@@ -1,10 +1,9 @@
 /*  Title:      Pure/General/completion.scala
     Author:     Makarius
 
-Semantic completion within the formal context (reported by prover).
+Semantic completion within the formal context (reported names).
 Syntactic completion of keywords and symbols, with abbreviations
-(based on language context).
-*/
+(based on language context).  */
 
 package isabelle
 
@@ -18,30 +17,21 @@
 {
   /** semantic completion **/
 
-  object Reported
+  object Names
   {
-    object Elem
+    object Info
     {
-      private def decode: XML.Decode.T[(String, List[String])] =
-      {
-        import XML.Decode._
-        pair(string, list(string))
-      }
-
-      def unapply(tree: XML.Tree): Option[Reported] =
-        tree match {
-          case XML.Elem(Markup(Markup.COMPLETION, _), body) =>
-            try {
-              val (original, replacements) = decode(body)
-              Some(Reported(original, replacements))
-            }
-            catch { case _: XML.Error => None }
+      def unapply(info: Text.Markup): Option[Names] =
+        info.info match {
+          case XML.Elem(Markup(Markup.COMPLETION,
+              (Markup.TOTAL, Properties.Value.Int(total)) :: names), _) =>
+            Some(Names(info.range, total, names.map(_._2)))
           case _ => None
         }
     }
   }
 
-  sealed case class Reported(original: String, replacements: List[String])
+  sealed case class Names(range: Text.Range, total: Int, names: List[String])