# HG changeset patch
# User wenzelm
# Date 1483028732 -3600
# Node ID d95b9117cb5bbfc9cb37ce68a77b3034cc07499a
# Parent  931f51fb24ca94803675d26d5f5aac1971379480
re-use resources from session;

diff -r 931f51fb24ca -r d95b9117cb5b src/Tools/VSCode/src/document_model.scala
--- a/src/Tools/VSCode/src/document_model.scala	Thu Dec 29 16:00:29 2016 +0100
+++ b/src/Tools/VSCode/src/document_model.scala	Thu Dec 29 17:25:32 2016 +0100
@@ -17,10 +17,9 @@
   changed: Boolean = true,
   published_diagnostics: List[Text.Info[Command.Results]] = Nil)
 {
-  override def toString: String = node_name.toString
+  /* name */
 
-
-  /* name */
+  override def toString: String = node_name.toString
 
   def uri: String = node_name.node
   def is_theory: Boolean = node_name.is_theory
@@ -28,11 +27,11 @@
 
   /* header */
 
-  def node_header(resources: VSCode_Resources): Document.Node.Header =
+  def node_header: Document.Node.Header =
     resources.special_header(node_name) getOrElse
     {
       if (is_theory)
-        session.resources.check_thy_reader(
+        resources.check_thy_reader(
           "", node_name, new CharSequenceReader(Thy_Header.header_text(doc)), Token.Pos.command)
       else Document.Node.no_header
     }
@@ -43,9 +42,9 @@
   def text_edits: List[Text.Edit] =
     if (changed) List(Text.Edit.insert(0, doc.make_text)) else Nil
 
-  def node_edits(resources: VSCode_Resources): List[Document.Edit_Text] =
+  def node_edits: List[Document.Edit_Text] =
     if (changed) {
-      List(session.header_edit(node_name, node_header(resources)),
+      List(session.header_edit(node_name, node_header),
         node_name -> Document.Node.Clear(),
         node_name -> Document.Node.Edits(text_edits),
         node_name ->
@@ -67,10 +66,12 @@
   }
 
 
-  /* snapshot and rendering */
+  /* session */
+
+  def resources: VSCode_Resources = session.resources.asInstanceOf[VSCode_Resources]
 
   def snapshot(): Document.Snapshot = session.snapshot(node_name, text_edits)
 
   def rendering(options: Options): VSCode_Rendering =
-    new VSCode_Rendering(this, snapshot(), options, session.resources)
+    new VSCode_Rendering(this, snapshot(), options, resources)
 }
diff -r 931f51fb24ca -r d95b9117cb5b src/Tools/VSCode/src/server.scala
--- a/src/Tools/VSCode/src/server.scala	Thu Dec 29 16:00:29 2016 +0100
+++ b/src/Tools/VSCode/src/server.scala	Thu Dec 29 17:25:32 2016 +0100
@@ -128,7 +128,7 @@
               model <- st.models.get(node_name.node)
               if model.changed } yield model).toList
           session.update(Document.Blobs.empty,
-            for { model <- changed; edit <- model.node_edits(resources) } yield edit)
+            for { model <- changed; edit <- model.node_edits } yield edit)
           st.copy(
             models = (st.models /: changed) { case (ms, m) => ms + (m.uri -> m.unchanged) },
             pending_input = Set.empty)
diff -r 931f51fb24ca -r d95b9117cb5b src/Tools/VSCode/src/vscode_rendering.scala
--- a/src/Tools/VSCode/src/vscode_rendering.scala	Thu Dec 29 16:00:29 2016 +0100
+++ b/src/Tools/VSCode/src/vscode_rendering.scala	Thu Dec 29 17:25:32 2016 +0100
@@ -38,7 +38,7 @@
     val model: Document_Model,
     snapshot: Document.Snapshot,
     options: Options,
-    resources: Resources)
+    resources: VSCode_Resources)
   extends Rendering(snapshot, options, resources)
 {
   /* diagnostics */