# HG changeset patch
# User wenzelm
# Date 1488560004 -3600
# Node ID 5f08197206cefb1311093ceda236a63867fe9822
# Parent  7672b29e544eb452db1e00c90f0fd55b1da3565b
clarified signature;

diff -r 7672b29e544e -r 5f08197206ce src/Tools/VSCode/src/protocol.scala
--- a/src/Tools/VSCode/src/protocol.scala	Fri Mar 03 11:07:27 2017 +0100
+++ b/src/Tools/VSCode/src/protocol.scala	Fri Mar 03 17:53:24 2017 +0100
@@ -205,6 +205,14 @@
   }
 
 
+  /* marked string */
+
+  sealed case class MarkedString(text: String, language: String = "plaintext")
+  {
+    def json: JSON.T = Map("language" -> language, "value" -> text)
+  }
+
+
   /* diagnostic messages */
 
   object MessageType
@@ -322,13 +330,12 @@
 
   object Hover extends RequestTextDocumentPosition("textDocument/hover")
   {
-    def reply(id: Id, result: Option[(Line.Range, List[String])]): JSON.T =
+    def reply(id: Id, result: Option[(Line.Range, List[MarkedString])]): JSON.T =
     {
       val res =
         result match {
           case Some((range, contents)) =>
-            Map("contents" -> contents.map(s => Map("language" -> "plaintext", "value" -> s)),
-              "range" -> Range(range))
+            Map("contents" -> contents.map(_.json), "range" -> Range(range))
           case None => Map("contents" -> Nil)
         }
       ResponseMessage(id, Some(res))
diff -r 7672b29e544e -r 5f08197206ce src/Tools/VSCode/src/server.scala
--- a/src/Tools/VSCode/src/server.scala	Fri Mar 03 11:07:27 2017 +0100
+++ b/src/Tools/VSCode/src/server.scala	Fri Mar 03 17:53:24 2017 +0100
@@ -300,7 +300,8 @@
         val doc = rendering.model.content.doc
         val range = doc.range(info.range)
         val contents =
-          info.info.map(tree => resources.output_pretty(List(tree), rendering.tooltip_margin))
+          info.info.map(tree =>
+            Protocol.MarkedString(resources.output_pretty(List(tree), rendering.tooltip_margin)))
         (range, contents)
       }
     channel.write(Protocol.Hover.reply(id, result))