--- 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))
--- 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))