src/Tools/VSCode/src/vscode_rendering.scala
changeset 64688 d8f194556c70
parent 64683 c0c09b6dfbe0
child 64702 d95b9117cb5b
--- 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))