diff -r 7e119f32276a -r c0c09b6dfbe0 src/Tools/VSCode/src/vscode_rendering.scala
--- a/src/Tools/VSCode/src/vscode_rendering.scala	Wed Dec 28 17:10:09 2016 +0100
+++ b/src/Tools/VSCode/src/vscode_rendering.scala	Wed Dec 28 17:26:38 2016 +0100
@@ -59,7 +59,7 @@
   {
     (for {
       Text.Info(text_range, res) <- results.iterator
-      range = model.doc.range(text_range, model.text_length)
+      range = model.doc.range(text_range)
       (_, XML.Elem(Markup(name, _), body)) <- res.iterator
     } yield {
       val message = Pretty.string_of(body, margin = diagnostics_margin)
@@ -89,10 +89,8 @@
         opt_text match {
           case Some(text) if range.start > 0 =>
             val chunk = Symbol.Text_Chunk(text)
-            val doc = Line.Document(text)
-            def position(offset: Symbol.Offset) =
-              doc.position(chunk.decode(offset), model.text_length)
-            Line.Range(position(range.start), position(range.stop))
+            val doc = Line.Document(text, model.doc.text_length)
+            doc.range(chunk.decode(range))
           case _ =>
             Line.Range(Line.Position((line1 - 1) max 0))
         })