# HG changeset patch
# User wenzelm
# Date 1393162791 -3600
# Node ID 78c83cd477c106e5ed5173d16eeeb42fb92f1fe3
# Parent  e99ed112d303d2ca0ed5f75f116dd8f86a88af97
clarified completion names;
tuned signature;

diff -r e99ed112d303 -r 78c83cd477c1 src/Pure/General/completion.ML
--- a/src/Pure/General/completion.ML	Sun Feb 23 10:44:57 2014 +0100
+++ b/src/Pure/General/completion.ML	Sun Feb 23 14:39:51 2014 +0100
@@ -6,32 +6,40 @@
 
 signature COMPLETION =
 sig
-  val limit: unit -> int
-  type T = {original: string, replacements: string list}
+  type T
+  val make: Position.T -> string list -> T
   val none: T
-  val reported_text: Position.T -> T -> string
-  val report: Position.T -> T -> unit
+  val report: T -> unit
 end;
 
 structure Completion: COMPLETION =
 struct
 
-fun limit () = Options.default_int "completion_limit";
-
+abstype T = Completion of {pos: Position.T, total: int, names: string list}
+with
 
-type T = {original: string, replacements: string list};
-
-val none: T = {original = "", replacements = []};
+fun dest (Completion args) = args;
 
-fun encode ({original, replacements}: T) =
-  (original, replacements)
-  |> let open XML.Encode in pair string (list string) end;
-
-fun reported_text pos (completion: T) =
-  if null (#replacements completion) then ""
-  else Position.reported_text pos Markup.completion (YXML.string_of_body (encode completion));
-
-fun report pos completion =
-  Output.report (reported_text pos completion);
+fun make pos names =
+  Completion
+   {pos = pos,
+    total = length names,
+    names = take (Options.default_int "completion_limit") names};
 
 end;
+
+val none = make Position.none [];
+
+fun report completion =
+  let val {pos, total, names} = dest completion in
+    if Position.is_reported pos andalso not (null names) then
+      let
+        val props =
+          (Markup.totalN, Markup.print_int total) ::
+            (map Markup.print_int (1 upto length names) ~~ names);
+        val markup = (Markup.completionN, Position.properties_of pos @ props);
+      in Output.report (Markup.markup markup "") end
+    else ()
+  end;
+
+end;
diff -r e99ed112d303 -r 78c83cd477c1 src/Pure/General/completion.scala
--- 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])
 
 
 
diff -r e99ed112d303 -r 78c83cd477c1 src/Pure/General/name_space.ML
--- a/src/Pure/General/name_space.ML	Sun Feb 23 10:44:57 2014 +0100
+++ b/src/Pure/General/name_space.ML	Sun Feb 23 14:39:51 2014 +0100
@@ -205,13 +205,12 @@
 fun completion context (space as Name_Space {internals, ...}) (xname, pos) =
   if Context_Position.is_visible_generic context andalso Position.is_reported pos then
     let
-      val replacements =
+      val names =
         Symtab.fold (fn (a, (b :: _, _)) => String.isPrefix xname a ? cons b | _ => I)
           internals []
-        |> take (Completion.limit ())
         |> map (extern_shortest (Context.proof_of context) space)
         |> sort_distinct string_ord;
-    in {original = xname, replacements = replacements} end
+    in Completion.make pos names end
   else Completion.none;
 
 
@@ -447,7 +446,7 @@
     (case Symtab.lookup tab name of
       SOME x => (Context_Position.report_generic context pos (markup space name); (name, x))
     | NONE =>
-       (Completion.report pos (completion context space (xname, pos));
+       (Completion.report (completion context space (xname, pos));
         error (undefined (kind_of space) name ^ Position.here pos)))
   end;
 
diff -r e99ed112d303 -r 78c83cd477c1 src/Pure/PIDE/markup.ML
--- a/src/Pure/PIDE/markup.ML	Sun Feb 23 10:44:57 2014 +0100
+++ b/src/Pure/PIDE/markup.ML	Sun Feb 23 14:39:51 2014 +0100
@@ -37,7 +37,8 @@
   val get_entity_kind: T -> string option
   val defN: string
   val refN: string
-  val completionN: string val completion: T
+  val totalN: string
+  val completionN: string
   val lineN: string
   val offsetN: string
   val end_offsetN: string
@@ -286,7 +287,8 @@
 
 (* completion *)
 
-val (completionN, completion) = markup_elem "completion";
+val totalN = "total";
+val completionN = "completion";
 
 
 (* position *)
diff -r e99ed112d303 -r 78c83cd477c1 src/Pure/PIDE/markup.scala
--- a/src/Pure/PIDE/markup.scala	Sun Feb 23 10:44:57 2014 +0100
+++ b/src/Pure/PIDE/markup.scala	Sun Feb 23 14:39:51 2014 +0100
@@ -69,6 +69,7 @@
 
   /* completion */
 
+  val TOTAL = "total"
   val COMPLETION = "completion"
 
 
diff -r e99ed112d303 -r 78c83cd477c1 src/Tools/jEdit/src/rendering.scala
--- a/src/Tools/jEdit/src/rendering.scala	Sun Feb 23 10:44:57 2014 +0100
+++ b/src/Tools/jEdit/src/rendering.scala	Sun Feb 23 14:39:51 2014 +0100
@@ -150,7 +150,7 @@
 
   /* markup elements */
 
-  private val completion_reported_elements = Set(Markup.COMPLETION)
+  private val completion_names_elements = Set(Markup.COMPLETION)
 
   private val completion_context_elements =
     Set(Markup.STRING, Markup.ALTSTRING, Markup.VERBATIM,
@@ -273,20 +273,17 @@
 
   /* completion */
 
-  def completion_reported(caret: Text.Offset): Option[Completion.Reported] =
-    if (caret > 0)
+  def completion_names(caret: Text.Offset): Option[Completion.Names] =
+    if (caret > 0 && !snapshot.is_outdated)
     {
       val result =
         snapshot.select(Text.Range(caret - 1, caret + 1),
-          Rendering.completion_reported_elements, _ =>
+          Rendering.completion_names_elements, _ =>
           {
-            case Text.Info(_, Completion.Reported.Elem(reported)) => Some(reported)
+            case Completion.Names.Info(names) => Some(names)
             case _ => None
           })
-      result match {
-        case Text.Info(_, reported) :: _ => Some(reported)
-        case Nil => None
-      }
+      result.headOption.map(_.info)
     }
     else None
 
@@ -304,10 +301,7 @@
             case Text.Info(_, _) =>
               Some(Completion.Context.inner)
           })
-      result match {
-        case Text.Info(_, context) :: _ => Some(context)
-        case Nil => None
-      }
+      result.headOption.map(_.info)
     }
     else None