# HG changeset patch
# User wenzelm
# Date 1495728796 -7200
# Node ID ab05479059b55bbf3a14a63b3ead4a1bfcbdb4e2
# Parent  d2f19f05c0e956c65c8d213a6af03dcb491b6817
tuned;

diff -r d2f19f05c0e9 -r ab05479059b5 src/Tools/VSCode/src/document_model.scala
--- a/src/Tools/VSCode/src/document_model.scala	Thu May 25 18:07:29 2017 +0200
+++ b/src/Tools/VSCode/src/document_model.scala	Thu May 25 18:13:16 2017 +0200
@@ -28,6 +28,11 @@
 
   /* content */
 
+  object Content
+  {
+    val empty: Content = Content(Line.Document.empty)
+  }
+
   sealed case class Content(doc: Line.Document)
   {
     override def toString: String = doc.toString
@@ -44,11 +49,7 @@
   }
 
   def init(session: Session, node_name: Document.Node.Name): Document_Model =
-  {
-    val resources = session.resources.asInstanceOf[VSCode_Resources]
-    val content = Content(Line.Document.empty)
-    Document_Model(session, node_name, content)
-  }
+    Document_Model(session, node_name, Content.empty)
 }
 
 sealed case class Document_Model(