--- a/src/Pure/PIDE/document.scala Sat Jan 07 20:44:37 2017 +0100
+++ b/src/Pure/PIDE/document.scala Sat Jan 07 21:32:00 2017 +0100
@@ -469,6 +469,8 @@
trait Model
{
def session: Session
+ def is_stable: Boolean
+ def snapshot(): Snapshot
def node_name: Document.Node.Name
def is_theory: Boolean = node_name.is_theory
@@ -477,12 +479,27 @@
def node_required: Boolean
def get_blob: Option[Document.Blob]
- def is_stable: Boolean
- def snapshot(): Snapshot
+ def node_header: Node.Header
+ def node_edits(
+ text_edits: List[Text.Edit], perspective: Node.Perspective_Text): List[Edit_Text] =
+ {
+ val edits: List[Node.Edit[Text.Edit, Text.Perspective]] =
+ get_blob match {
+ case None =>
+ List(
+ Document.Node.Deps(
+ if (session.resources.loaded_theories(node_name.theory))
+ node_header.error("Cannot update finished theory " + quote(node_name.theory))
+ else node_header),
+ Document.Node.Edits(text_edits), perspective)
+ case Some(blob) =>
+ List(Document.Node.Blob(blob), Document.Node.Edits(text_edits))
+ }
+ edits.flatMap(edit => if (edit.is_void) None else Some(node_name -> edit))
+ }
}
-
/** global state -- document structure, execution process, editing history **/
type Assign_Update =