# HG changeset patch
# User wenzelm
# Date 1483741518 -3600
# Node ID c7693244672e9cba6d33321961ff4e8d5a1b94ff
# Parent  7283f41d05abf5d010dbdd3c030fb89b723c38a9
tuned;

diff -r 7283f41d05ab -r c7693244672e src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Fri Jan 06 13:27:18 2017 +0100
+++ b/src/Pure/PIDE/document.scala	Fri Jan 06 23:25:18 2017 +0100
@@ -467,6 +467,24 @@
   }
 
 
+  /* model */
+
+  trait Model
+  {
+    /*session*/
+    def session: Session
+    def snapshot(): Snapshot
+
+    /*name*/
+    def node_name: Document.Node.Name
+    def is_theory: Boolean = node_name.is_theory
+    override def toString: String = node_name.toString
+
+    /*content*/
+    def get_blob: Option[Document.Blob]
+  }
+
+
 
   /** global state -- document structure, execution process, editing history **/
 
diff -r 7283f41d05ab -r c7693244672e src/Tools/VSCode/src/document_model.scala
--- a/src/Tools/VSCode/src/document_model.scala	Fri Jan 06 13:27:18 2017 +0100
+++ b/src/Tools/VSCode/src/document_model.scala	Fri Jan 06 23:25:18 2017 +0100
@@ -32,15 +32,8 @@
   node_required: Boolean = false,
   last_perspective: Document.Node.Perspective_Text = Document.Node.no_perspective_text,
   pending_edits: Vector[Text.Edit] = Vector.empty,
-  published_diagnostics: List[Text.Info[Command.Results]] = Nil)
+  published_diagnostics: List[Text.Info[Command.Results]] = Nil) extends Document.Model
 {
-  /* name */
-
-  override def toString: String = node_name.toString
-
-  def is_theory: Boolean = node_name.is_theory
-
-
   /* external file */
 
   def external(b: Boolean): Document_Model = copy(external_file = b)