# HG changeset patch # User wenzelm # Date 1488655592 -3600 # Node ID 1f47b92021debbd211a7d7519a0f12c2250ca447 # Parent 66b19d05dcee4175af2ed2df156e77abf9a5dfb8 clarified signature; diff -r 66b19d05dcee -r 1f47b92021de src/Tools/VSCode/src/document_model.scala --- a/src/Tools/VSCode/src/document_model.scala Sat Mar 04 13:36:06 2017 +0100 +++ b/src/Tools/VSCode/src/document_model.scala Sat Mar 04 20:26:32 2017 +0100 @@ -16,7 +16,7 @@ { /* decorations */ - sealed case class Decoration(typ: String, content: List[Text.Info[XML.Body]]) + sealed case class Decoration(typ: String, content: List[Text.Info[List[XML.Body]]]) /* content */ diff -r 66b19d05dcee -r 1f47b92021de src/Tools/VSCode/src/vscode_rendering.scala --- a/src/Tools/VSCode/src/vscode_rendering.scala Sat Mar 04 13:36:06 2017 +0100 +++ b/src/Tools/VSCode/src/vscode_rendering.scala Sat Mar 04 20:26:32 2017 +0100 @@ -17,20 +17,16 @@ { /* decorations */ - def color_decorations(prefix: String, types: Rendering.Color.ValueSet, + private def color_decorations(prefix: String, types: Rendering.Color.ValueSet, colors: List[Text.Info[Rendering.Color.Value]]): List[Document_Model.Decoration] = { val color_ranges = (Map.empty[Rendering.Color.Value, List[Text.Range]] /: colors) { case (m, Text.Info(range, c)) => m + (c -> (range :: m.getOrElse(c, Nil))) } - for (c <- types.toList) - yield { - val typ = prefix + c.toString - val content = - color_ranges.getOrElse(c, Nil).reverse.map(r => Text.Info(r, Nil: XML.Body)) - Document_Model.Decoration(typ, content) - } + types.toList.map(c => + Document_Model.Decoration(prefix + c.toString, + color_ranges.getOrElse(c, Nil).reverse.map(r => Text.Info(r, Nil: List[XML.Body])))) } @@ -127,7 +123,7 @@ val content = snapshot.select(model.content.text_range, VSCode_Rendering.bad_elements, _ => { - case Text.Info(_, XML.Elem(_, body)) => Some(body) + case Text.Info(_, XML.Elem(_, body)) => Some(List(body)) }) List(Document_Model.Decoration(Protocol.Decorations.bad, content)) } @@ -135,11 +131,12 @@ def decoration_output(decoration: Document_Model.Decoration): Protocol.Decoration = { val content = - for (Text.Info(text_range, body) <- decoration.content) + for (Text.Info(text_range, msgs) <- decoration.content) yield { val range = model.content.doc.range(text_range) - val msg = resources.output_pretty(body, diagnostics_margin) - Protocol.DecorationOptions(range, if (msg == "") Nil else List(Protocol.MarkedString(msg))) + Protocol.DecorationOptions(range, + msgs.map(msg => + Protocol.MarkedString(resources.output_pretty(msg, diagnostics_margin)))) } Protocol.Decoration(decoration.typ, content) }