--- 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(