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(