# HG changeset patch
# User wenzelm
# Date 1483352786 -3600
# Node ID 54afac94f52b0013b17ab21c08d90d7929d67871
# Parent  34db87033abed785370d0168be95951d3f4ce3da
proper content format;

diff -r 34db87033abe -r 54afac94f52b src/Tools/VSCode/src/protocol.scala
--- a/src/Tools/VSCode/src/protocol.scala	Mon Jan 02 10:59:46 2017 +0100
+++ b/src/Tools/VSCode/src/protocol.scala	Mon Jan 02 11:26:26 2017 +0100
@@ -296,7 +296,9 @@
     {
       val res =
         result match {
-          case Some((range, contents)) => Map("contents" -> contents, "range" -> Range(range))
+          case Some((range, contents)) =>
+            Map("contents" -> contents.map(s => Map("language" -> "plaintext", "value" -> s)),
+              "range" -> Range(range))
           case None => Map("contents" -> Nil)
         }
       ResponseMessage(id, Some(res))
diff -r 34db87033abe -r 54afac94f52b src/Tools/VSCode/src/server.scala
--- a/src/Tools/VSCode/src/server.scala	Mon Jan 02 10:59:46 2017 +0100
+++ b/src/Tools/VSCode/src/server.scala	Mon Jan 02 11:26:26 2017 +0100
@@ -285,7 +285,7 @@
         val doc = rendering.model.doc
         val range = doc.range(info.range)
         val s = Pretty.string_of(info.info, margin = rendering.tooltip_margin)
-        (range, List("```\n" + s + "\n```"))  // FIXME proper content format
+        (range, List(s))
       }
     channel.write(Protocol.Hover.reply(id, result))
   }