# HG changeset patch
# User wenzelm
# Date 1426516412 -3600
# Node ID 44a3ed0b82653c4daeee3a9cdefcc2cc841353b0
# Parent  8c56b34a88b019b92ec65adf849e4206fd00ea2b
support for completion reports produced in Scala (inlined into messages);

diff -r 8c56b34a88b0 -r 44a3ed0b8265 src/Pure/General/completion.scala
--- a/src/Pure/General/completion.scala	Mon Mar 16 14:15:15 2015 +0100
+++ b/src/Pure/General/completion.scala	Mon Mar 16 15:33:32 2015 +0100
@@ -135,10 +135,31 @@
 
   /** semantic completion **/
 
+  def report_no_completion(pos: Position.T): String =
+    YXML.string_of_tree(Semantic.Info(pos, No_Completion))
+
+  def report_names(pos: Position.T, total: Int, names: List[(String, (String, String))]): String =
+    YXML.string_of_tree(Semantic.Info(pos, Names(total, names)))
+
   object Semantic
   {
     object Info
     {
+      def apply(pos: Position.T, semantic: Semantic): XML.Elem =
+      {
+        val elem =
+          semantic match {
+            case No_Completion => XML.Elem(Markup(Markup.NO_COMPLETION, pos), Nil)
+            case Names(total, names) =>
+              XML.Elem(Markup(Markup.COMPLETION, pos),
+                {
+                  import XML.Encode._
+                  pair(int, list(pair(string, pair(string, string))))(total, names)
+                })
+          }
+        XML.Elem(Markup(Markup.REPORT, pos), List(elem))
+      }
+
       def unapply(info: Text.Markup): Option[Text.Info[Semantic]] =
         info.info match {
           case XML.Elem(Markup(Markup.COMPLETION, _), body) =>