src/Tools/VSCode/src/server.scala

--- a/src/Tools/VSCode/src/server.scala	Sun Mar 12 14:23:38 2017 +0100
+++ b/src/Tools/VSCode/src/server.scala	Sun Mar 12 14:31:29 2017 +0100
@@ -312,8 +312,7 @@
         (rendering, offset) <- rendering_offset(node_pos)
         info <- rendering.tooltips(VSCode_Rendering.tooltip_elements, Text.Range(offset, offset + 1))
       } yield {
-        val doc = rendering.model.content.doc
-        val range = doc.range(info.range)
+        val range = rendering.model.content.doc.range(info.range)
         val contents =
           info.info.map(t => Protocol.MarkedString(resources.output_pretty_tooltip(List(t))))
         (range, contents)
@@ -340,9 +339,9 @@
     val result =
       (for ((rendering, offset) <- rendering_offset(node_pos))
         yield {
-          val doc = rendering.model.content.doc
-          rendering.caret_focus_ranges(Text.Range(offset, offset + 1), doc.text_range)
-            .map(r => Protocol.DocumentHighlight.text(doc.range(r)))
+          val model = rendering.model
+          rendering.caret_focus_ranges(Text.Range(offset, offset + 1), model.content.text_range)
+            .map(r => Protocol.DocumentHighlight.text(model.content.doc.range(r)))
         }) getOrElse Nil
     channel.write(Protocol.DocumentHighlights.reply(id, result))
   }