# HG changeset patch
# User wenzelm
# Date 1482948952 -3600
# Node ID d8f194556c70594c4cd1e5be3c6fec6ea9d4cac2
# Parent  04806ad1e43a767644ebdcccb0f1fd1b8c2815dc
precise full_range and thus proper try_restrict in Snapshot.cumulate;

diff -r 04806ad1e43a -r d8f194556c70 src/Pure/PIDE/line.scala
--- a/src/Pure/PIDE/line.scala	Wed Dec 28 17:54:55 2016 +0100
+++ b/src/Pure/PIDE/line.scala	Wed Dec 28 19:15:52 2016 +0100
@@ -131,6 +131,12 @@
       }
       else None
     }
+
+    lazy val end_offset: Text.Offset =
+      if (lines.isEmpty) 0
+      else ((0 /: lines) { case (n, line) => n + text_length(line.text) + 1 }) - 1
+
+    def full_range: Text.Range = Text.Range(0, end_offset)
   }
 
 
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))