proper content format;
authorwenzelm
Mon Jan 02 11:26:26 2017 +0100 (2017-01-02)
changeset 6474754afac94f52b
parent 64746 34db87033abe
child 64748 155bf8632104
proper content format;
src/Tools/VSCode/src/protocol.scala
src/Tools/VSCode/src/server.scala
     1.1 --- a/src/Tools/VSCode/src/protocol.scala	Mon Jan 02 10:59:46 2017 +0100
     1.2 +++ b/src/Tools/VSCode/src/protocol.scala	Mon Jan 02 11:26:26 2017 +0100
     1.3 @@ -296,7 +296,9 @@
     1.4      {
     1.5        val res =
     1.6          result match {
     1.7 -          case Some((range, contents)) => Map("contents" -> contents, "range" -> Range(range))
     1.8 +          case Some((range, contents)) =>
     1.9 +            Map("contents" -> contents.map(s => Map("language" -> "plaintext", "value" -> s)),
    1.10 +              "range" -> Range(range))
    1.11            case None => Map("contents" -> Nil)
    1.12          }
    1.13        ResponseMessage(id, Some(res))
     2.1 --- a/src/Tools/VSCode/src/server.scala	Mon Jan 02 10:59:46 2017 +0100
     2.2 +++ b/src/Tools/VSCode/src/server.scala	Mon Jan 02 11:26:26 2017 +0100
     2.3 @@ -285,7 +285,7 @@
     2.4          val doc = rendering.model.doc
     2.5          val range = doc.range(info.range)
     2.6          val s = Pretty.string_of(info.info, margin = rendering.tooltip_margin)
     2.7 -        (range, List("```\n" + s + "\n```"))  // FIXME proper content format
     2.8 +        (range, List(s))
     2.9        }
    2.10      channel.write(Protocol.Hover.reply(id, result))
    2.11    }