src/Pure/PIDE/document.scala

     def select[A](
       range: Text.Range,
       elements: Markup.Elements,
       result: List[Command.State] => Text.Markup => Option[A],
       status: Boolean = false): List[Text.Info[A]]
+  }
+
+
+  /* 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 **/