# HG changeset patch # User wenzelm # Date 1488630827 -3600 # Node ID 0bf1836ce4b1602afda179413d3340fa3888ddb2 # Parent 136b620b11afae64752aeb38a3205a49f9e1c8a2 tight protocol messages; diff -r 136b620b11af -r 0bf1836ce4b1 src/Tools/VSCode/src/protocol.scala --- a/src/Tools/VSCode/src/protocol.scala Sat Mar 04 09:29:24 2017 +0100 +++ b/src/Tools/VSCode/src/protocol.scala Sat Mar 04 13:33:47 2017 +0100 @@ -205,13 +205,23 @@ } - /* marked string */ + /* marked strings */ sealed case class MarkedString(text: String, language: String = "plaintext") { def json: JSON.T = Map("language" -> language, "value" -> text) } + object MarkedStrings + { + def json(msgs: List[MarkedString]): Option[JSON.T] = + msgs match { + case Nil => None + case List(msg) => Some(msg.json) + case _ => Some(msgs.map(_.json)) + } + } + /* diagnostic messages */ @@ -335,7 +345,7 @@ val res = result match { case Some((range, contents)) => - Map("contents" -> contents.map(_.json), "range" -> Range(range)) + Map("contents" -> MarkedStrings.json(contents).getOrElse(Nil), "range" -> Range(range)) case None => Map("contents" -> Nil) } ResponseMessage(id, Some(res)) @@ -414,16 +424,19 @@ sealed case class DecorationOptions(range: Line.Range, hover_message: List[MarkedString]) { + def no_hover_message: Boolean = hover_message.isEmpty + def json_range: JSON.T = Range(range) def json: JSON.T = - Map("range" -> Range(range)) ++ - JSON.optional("hoverMessage" -> - (if (hover_message.isEmpty) None else Some(hover_message.map(_.json)))) + Map("range" -> json_range) ++ + JSON.optional("hoverMessage" -> MarkedStrings.json(hover_message)) } sealed case class Decoration(typ: String, content: List[DecorationOptions]) { + def json_content: JSON.T = + if (content.forall(_.no_hover_message)) content.map(_.json_range) else content.map(_.json) def json(file: JFile): JSON.T = Notification("PIDE/decoration", - Map("uri" -> Url.print_file(file), "type" -> typ, "content" -> content.map(_.json))) + Map("uri" -> Url.print_file(file), "type" -> typ, "content" -> json_content)) } }