diff -r 04806ad1e43a -r d8f194556c70 src/Tools/VSCode/src/vscode_rendering.scala --- 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))