# HG changeset patch
# User wenzelm
# Date 1393186319 -3600
# Node ID a1184dfb8e0020b3258b7538f7ed188efe81809d
# Parent  93ba0085e888048ebaabb210f4734c1b07c20174
clarified semantic completion: retain kind.full_name as official item name for history;
misc tuning;

diff -r 93ba0085e888 -r a1184dfb8e00 src/Pure/General/completion.ML
--- a/src/Pure/General/completion.ML	Sun Feb 23 20:24:33 2014 +0100
+++ b/src/Pure/General/completion.ML	Sun Feb 23 21:11:59 2014 +0100
@@ -7,7 +7,7 @@
 signature COMPLETION =
 sig
   type T
-  val make: Position.T -> string list -> T
+  val names: Position.T -> (string * string) list -> T
   val none: T
   val report: T -> unit
 end;
@@ -15,12 +15,12 @@
 structure Completion: COMPLETION =
 struct
 
-abstype T = Completion of {pos: Position.T, total: int, names: string list}
+abstype T = Completion of {pos: Position.T, total: int, names: (string * string) list}
 with
 
 fun dest (Completion args) = args;
 
-fun make pos names =
+fun names pos names =
   Completion
    {pos = pos,
     total = length names,
@@ -28,17 +28,16 @@
 
 end;
 
-val none = make Position.none [];
+val none = names 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
+        val markup = Position.markup pos Markup.completion;
+        val body = (total, names) |>
+          let open XML.Encode in pair int (list (pair string string)) end;
+      in Output.report (YXML.string_of (XML.Elem (markup, body))) end
     else ()
   end;
 
diff -r 93ba0085e888 -r a1184dfb8e00 src/Pure/General/completion.scala
--- a/src/Pure/General/completion.scala	Sun Feb 23 20:24:33 2014 +0100
+++ b/src/Pure/General/completion.scala	Sun Feb 23 21:11:59 2014 +0100
@@ -15,71 +15,17 @@
 
 object Completion
 {
-  /** semantic completion **/
-
-  object Names
-  {
-    object Info
-    {
-      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 Names(range: Text.Range, total: Int, names: List[String])
-  {
-    def complete(
-      history: Completion.History,
-      decode: Boolean,
-      original: String): Option[Completion.Result] =
-    {
-      val items =
-        for {
-          raw_name <- names
-          name = (if (decode) Symbol.decode(raw_name) else raw_name)
-          if name != original
-        } yield Item(range, original, name, name, 0, true)
-
-      if (items.isEmpty) None
-      else Some(Result(range, original, names.length == 1, items))
-    }
-  }
-
-
-
-  /** syntactic completion **/
-
-  /* language context */
-
-  object Context
-  {
-    val outer = Context("", true, false)
-    val inner = Context(Markup.Language.UNKNOWN, true, false)
-    val ML_outer = Context(Markup.Language.ML, false, false)
-    val ML_inner = Context(Markup.Language.ML, true, true)
-  }
-
-  sealed case class Context(language: String, symbols: Boolean, antiquotes: Boolean)
-  {
-    def is_outer: Boolean = language == ""
-  }
-
-
-  /* result */
+  /** completion result **/
 
   sealed case class Item(
     range: Text.Range,
     original: String,
     name: String,
+    description: String,
     replacement: String,
     move: Int,
     immediate: Boolean)
-  { override def toString: String = name }
+  { override def toString: String = description }
 
   sealed case class Result(
     range: Text.Range,
@@ -88,11 +34,6 @@
     items: List[Item])
 
 
-  /* init */
-
-  val empty: Completion = new Completion()
-  def init(): Completion = empty.add_symbols()
-
 
   /** persistent history **/
 
@@ -176,7 +117,76 @@
   }
 
 
-  /** word parsers **/
+
+  /** semantic completion **/
+
+  object Names
+  {
+    object Info
+    {
+      def unapply(info: Text.Markup): Option[Names] =
+        info.info match {
+          case XML.Elem(Markup(Markup.COMPLETION, _), body) =>
+            try {
+              val (total, names) =
+              {
+                import XML.Decode._
+                pair(int, list(pair(string, string)))(body)
+              }
+              Some(Names(info.range, total, names))
+            }
+            catch { case _: XML.Error => None }
+          case _ => None
+        }
+    }
+  }
+
+  sealed case class Names(range: Text.Range, total: Int, names: List[(String, String)])
+  {
+    def complete(
+      history: Completion.History,
+      decode: Boolean,
+      original: String): Option[Completion.Result] =
+    {
+      val items =
+        for {
+          (xname, name) <- names
+          xname1 = (if (decode) Symbol.decode(xname) else xname)
+          if xname1 != original
+        } yield Item(range, original, name, xname1, xname1, 0, true)
+
+      if (items.isEmpty) None
+      else Some(Result(range, original, names.length == 1, items.sorted(history.ordering)))
+    }
+  }
+
+
+
+  /** syntactic completion **/
+
+  /* language context */
+
+  object Context
+  {
+    val outer = Context("", true, false)
+    val inner = Context(Markup.Language.UNKNOWN, true, false)
+    val ML_outer = Context(Markup.Language.ML, false, false)
+    val ML_inner = Context(Markup.Language.ML, true, true)
+  }
+
+  sealed case class Context(language: String, symbols: Boolean, antiquotes: Boolean)
+  {
+    def is_outer: Boolean = language == ""
+  }
+
+
+  /* init */
+
+  val empty: Completion = new Completion()
+  def init(): Completion = empty.add_symbols()
+
+
+  /* word parsers */
 
   private object Word_Parsers extends RegexParsers
   {
@@ -313,7 +323,7 @@
                   case List(s1, s2) => (s1, s2)
                   case _ => (s, "")
                 }
-              Completion.Item(range, word, s, s1 + s2, - s2.length, explicit || immediate)
+              Completion.Item(range, word, s, s, s1 + s2, - s2.length, explicit || immediate)
             })
           Some(Completion.Result(range, word, cs.length == 1, items.sorted(history.ordering)))
         }
diff -r 93ba0085e888 -r a1184dfb8e00 src/Pure/General/name_space.ML
--- a/src/Pure/General/name_space.ML	Sun Feb 23 20:24:33 2014 +0100
+++ b/src/Pure/General/name_space.ML	Sun Feb 23 21:11:59 2014 +0100
@@ -202,15 +202,18 @@
 
 (* completion *)
 
-fun completion context (space as Name_Space {internals, ...}) (xname, pos) =
-  if Context_Position.is_visible_generic context andalso Position.is_reported pos then
+fun completion context space (xname, pos) =
+  if Context_Position.is_visible_generic context andalso Position.is_reported pos
+  then
     let
+      val Name_Space {kind = k, internals, ...} = space;
+      val ext = extern_shortest (Context.proof_of context) space;
       val names =
-        Symtab.fold (fn (a, (b :: _, _)) => String.isPrefix xname a ? cons b | _ => I)
-          internals []
-        |> map (extern_shortest (Context.proof_of context) space)
-        |> sort_distinct string_ord;
-    in Completion.make pos names end
+        Symtab.fold
+          (fn (a, (b :: _, _)) => String.isPrefix xname a ? cons (ext b, Long_Name.implode [k, b])
+            | _ => I) internals []
+        |> sort_distinct (string_ord o pairself #1);
+    in Completion.names pos names end
   else Completion.none;
 
 
diff -r 93ba0085e888 -r a1184dfb8e00 src/Pure/PIDE/markup.ML
--- a/src/Pure/PIDE/markup.ML	Sun Feb 23 20:24:33 2014 +0100
+++ b/src/Pure/PIDE/markup.ML	Sun Feb 23 21:11:59 2014 +0100
@@ -37,8 +37,7 @@
   val get_entity_kind: T -> string option
   val defN: string
   val refN: string
-  val totalN: string
-  val completionN: string
+  val completionN: string val completion: T
   val lineN: string
   val offsetN: string
   val end_offsetN: string
@@ -287,8 +286,7 @@
 
 (* completion *)
 
-val totalN = "total";
-val completionN = "completion";
+val (completionN, completion) = markup_elem "completion";
 
 
 (* position *)
diff -r 93ba0085e888 -r a1184dfb8e00 src/Pure/PIDE/markup.scala
--- a/src/Pure/PIDE/markup.scala	Sun Feb 23 20:24:33 2014 +0100
+++ b/src/Pure/PIDE/markup.scala	Sun Feb 23 21:11:59 2014 +0100
@@ -69,7 +69,6 @@
 
   /* completion */
 
-  val TOTAL = "total"
   val COMPLETION = "completion"