--- a/src/Tools/VSCode/src/vscode_rendering.scala Wed Dec 28 17:54:55 2016 +0100
+++ b/src/Tools/VSCode/src/vscode_rendering.scala Wed Dec 28 19:15:52 2016 +0100
@@ -45,7 +45,7 @@
def diagnostics: List[Text.Info[Command.Results]] =
snapshot.cumulate[Command.Results](
- Text.Range.full, Command.Results.empty, VSCode_Rendering.diagnostics_elements, _ =>
+ model.doc.full_range, Command.Results.empty, VSCode_Rendering.diagnostics_elements, _ =>
{
case (res, Text.Info(_, msg @ XML.Elem(Markup(_, Markup.Serial(i)), body)))
if body.nonEmpty => Some(res + (i -> msg))