# HG changeset patch
# User wenzelm
# Date 1497972497 -7200
# Node ID 51f74025a3e366da2e7d0352ff710e6ce06485ae
# Parent  90629b166203ba8a5a97fecdd72a40a1f7752d4b
tuned signature;

diff -r 90629b166203 -r 51f74025a3e3 src/Tools/VSCode/src/vscode_rendering.scala
--- a/src/Tools/VSCode/src/vscode_rendering.scala	Tue Jun 20 17:14:27 2017 +0200
+++ b/src/Tools/VSCode/src/vscode_rendering.scala	Tue Jun 20 17:28:17 2017 +0200
@@ -71,6 +71,7 @@
   rendering =>
 
   def model: Document_Model = _model
+  def resources: VSCode_Resources = model.resources
 
 
   /* completion */
@@ -136,7 +137,7 @@
       range = model.content.doc.range(text_range)
       (_, XML.Elem(Markup(name, _), body)) <- res.iterator
     } yield {
-      val message = model.resources.output_pretty_message(body)
+      val message = resources.output_pretty_message(body)
       val severity = VSCode_Rendering.message_severity.get(name)
       Protocol.Diagnostic(range, message, severity = severity)
     }).toList
@@ -222,7 +223,7 @@
       yield {
         val range = model.content.doc.range(text_range)
         Protocol.DecorationOpts(range,
-          msgs.map(msg => Protocol.MarkedString(model.resources.output_pretty_tooltip(msg))))
+          msgs.map(msg => Protocol.MarkedString(resources.output_pretty_tooltip(msg))))
       }
     Protocol.Decoration(decoration.typ, content)
   }
@@ -239,7 +240,7 @@
     : Option[Line.Node_Range] =
   {
     for {
-      platform_path <- model.resources.source_file(source_name)
+      platform_path <- resources.source_file(source_name)
       file <-
         (try { Some(new JFile(platform_path).getCanonicalFile) }
          catch { case ERROR(_) => None })
@@ -247,7 +248,7 @@
     yield {
       Line.Node_Range(file.getPath,
         if (range.start > 0) {
-          model.resources.get_file_content(file) match {
+          resources.get_file_content(file) match {
             case Some(text) =>
               val chunk = Symbol.Text_Chunk(text)
               val doc = Line.Document(text)
@@ -302,7 +303,7 @@
           case (links, Text.Info(info_range, XML.Elem(Markup.Citation(name), _))) =>
             val iterator =
               for {
-                Text.Info(entry_range, (entry, model)) <- model.resources.bibtex_entries_iterator
+                Text.Info(entry_range, (entry, model)) <- resources.bibtex_entries_iterator
                 if entry == name
               } yield Line.Node_Range(model.node_name.node, model.content.doc.range(entry_range))
             if (iterator.isEmpty) None else Some((links /: iterator)(_ :+ _))
diff -r 90629b166203 -r 51f74025a3e3 src/Tools/VSCode/src/vscode_spell_checker.scala
--- a/src/Tools/VSCode/src/vscode_spell_checker.scala	Tue Jun 20 17:14:27 2017 +0200
+++ b/src/Tools/VSCode/src/vscode_spell_checker.scala	Tue Jun 20 17:28:17 2017 +0200
@@ -17,7 +17,7 @@
     val model = rendering.model
     val ranges =
       (for {
-        spell_checker <- model.resources.spell_checker.get.iterator
+        spell_checker <- rendering.resources.spell_checker.get.iterator
         spell_range <- rendering.spell_checker_ranges(model.content.text_range).iterator
         text <- model.try_get_text(spell_range).iterator
         info <- spell_checker.marked_words(spell_range.start, text).iterator
@@ -26,14 +26,13 @@
   }
 
   def completion(rendering: VSCode_Rendering, caret: Text.Offset): Option[Completion.Result] =
-    rendering.model.resources.spell_checker.get.flatMap(_.completion(rendering, caret))
+    rendering.resources.spell_checker.get.flatMap(_.completion(rendering, caret))
 
   def menu_items(rendering: VSCode_Rendering, caret: Text.Offset): List[Protocol.CompletionItem] =
   {
-    val model = rendering.model
     val result =
       for {
-        spell_checker <- model.resources.spell_checker.get
+        spell_checker <- rendering.resources.spell_checker.get
         range = rendering.before_caret_range(caret)
         Text.Info(_, word) <- Spell_Checker.current_word(rendering, range)
       } yield (spell_checker, word)
@@ -45,7 +44,7 @@
           Protocol.CompletionItem(
             label = command.title,
             text = Some(""),
-            range = Some(model.content.doc.range(Text.Range(caret))),
+            range = Some(rendering.model.content.doc.range(Text.Range(caret))),
             command = Some(command))
 
         val update_items =