--- a/src/Tools/VSCode/extension/src/decorations.ts Sat Mar 04 20:26:32 2017 +0100
+++ b/src/Tools/VSCode/extension/src/decorations.ts Sat Mar 04 21:04:44 2017 +0100
@@ -61,7 +61,7 @@
for (let color of foreground_colors) {
types["foreground_".concat(color)] = background(color) // approximation
}
- types["bad"] = decoration({})
+ types["hover_message"] = decoration({})
}
--- a/src/Tools/VSCode/src/protocol.scala Sat Mar 04 20:26:32 2017 +0100
+++ b/src/Tools/VSCode/src/protocol.scala Sat Mar 04 21:04:44 2017 +0100
@@ -417,11 +417,6 @@
/* decorations */
- object Decorations
- {
- val bad = "bad"
- }
-
sealed case class DecorationOptions(range: Line.Range, hover_message: List[MarkedString])
{
def no_hover_message: Boolean = hover_message.isEmpty
--- a/src/Tools/VSCode/src/vscode_rendering.scala Sat Mar 04 20:26:32 2017 +0100
+++ b/src/Tools/VSCode/src/vscode_rendering.scala Sat Mar 04 21:04:44 2017 +0100
@@ -46,7 +46,7 @@
private val diagnostics_elements =
Markup.Elements(Markup.WRITELN, Markup.INFORMATION, Markup.WARNING, Markup.LEGACY, Markup.ERROR)
- private val bad_elements = Markup.Elements(Markup.BAD)
+ private val hover_message_elements = Markup.Elements(Markup.BAD)
private val hyperlink_elements =
Markup.Elements(Markup.ENTITY, Markup.PATH, Markup.POSITION, Markup.CITATION)
@@ -111,23 +111,32 @@
/* decorations */
+ def hover_message: Document_Model.Decoration =
+ {
+ val results =
+ snapshot.cumulate[Command.Results](
+ model.content.text_range, Command.Results.empty,
+ VSCode_Rendering.hover_message_elements, _ =>
+ {
+ case (msgs, Text.Info(_, XML.Elem(Markup(name, props @ Markup.Serial(serial)), body)))
+ if body.nonEmpty =>
+ Some(msgs + (serial -> XML.Elem(Markup(Markup.message(name), props), body)))
+
+ case _ => None
+ })
+ val content =
+ for (Text.Info(r, msgs) <- results if !msgs.is_empty)
+ yield Text.Info(r, (for ((_, t) <- msgs.iterator) yield List(t)).toList)
+ Document_Model.Decoration("hover_message", content)
+ }
+
def decorations: List[Document_Model.Decoration] =
- decorations_bad :::
+ hover_message ::
VSCode_Rendering.color_decorations("background_", Rendering.Color.background,
background(model.content.text_range, Set.empty)) :::
VSCode_Rendering.color_decorations("foreground_", Rendering.Color.foreground,
foreground(model.content.text_range))
- def decorations_bad: List[Document_Model.Decoration] =
- {
- val content =
- snapshot.select(model.content.text_range, VSCode_Rendering.bad_elements, _ =>
- {
- case Text.Info(_, XML.Elem(_, body)) => Some(List(body))
- })
- List(Document_Model.Decoration(Protocol.Decorations.bad, content))
- }
-
def decoration_output(decoration: Document_Model.Decoration): Protocol.Decoration =
{
val content =