# HG changeset patch
# User wenzelm
# Date 1483821120 -3600
# Node ID 4ef1eb75f1cd370a0db17e2ef2299109c6591086
# Parent  c97296294f6dc7c041043a2a94f8e061efdf5efc
uniform Document.Model.node_edits (without void edits);

diff -r c97296294f6d -r 4ef1eb75f1cd src/Pure/PIDE/document.scala
--- 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 =
diff -r c97296294f6d -r 4ef1eb75f1cd src/Pure/PIDE/session.scala
--- a/src/Pure/PIDE/session.scala	Sat Jan 07 20:44:37 2017 +0100
+++ b/src/Pure/PIDE/session.scala	Sat Jan 07 21:32:00 2017 +0100
@@ -242,18 +242,6 @@
     resources.base_syntax
 
 
-  /* theory files */
-
-  def header_edit(name: Document.Node.Name, header: Document.Node.Header): Document.Edit_Text =
-  {
-    val header1 =
-      if (resources.loaded_theories(name.theory))
-        header.error("Cannot update finished theory " + quote(name.theory))
-      else header
-    (name, Document.Node.Deps(header1))
-  }
-
-
   /* pipelined change parsing */
 
   private case class Text_Edits(
diff -r c97296294f6d -r 4ef1eb75f1cd src/Tools/VSCode/src/document_model.scala
--- a/src/Tools/VSCode/src/document_model.scala	Sat Jan 07 20:44:37 2017 +0100
+++ b/src/Tools/VSCode/src/document_model.scala	Sat Jan 07 21:32:00 2017 +0100
@@ -91,16 +91,7 @@
   {
     val (reparse, perspective) = node_perspective(doc_blobs)
     if (reparse || pending_edits.nonEmpty || last_perspective != perspective) {
-      val edits: List[Document.Edit_Text] =
-        get_blob match {
-          case None =>
-            List(session.header_edit(node_name, node_header),
-              node_name -> Document.Node.Edits(pending_edits),
-              node_name -> perspective)
-          case Some(blob) =>
-            List(node_name -> Document.Node.Blob(blob),
-              node_name -> Document.Node.Edits(pending_edits))
-        }
+      val edits = node_edits(pending_edits, perspective)
       Some((edits, copy(pending_edits = Nil, last_perspective = perspective)))
     }
     else None
diff -r c97296294f6d -r 4ef1eb75f1cd src/Tools/jEdit/src/document_model.scala
--- a/src/Tools/jEdit/src/document_model.scala	Sat Jan 07 20:44:37 2017 +0100
+++ b/src/Tools/jEdit/src/document_model.scala	Sat Jan 07 21:32:00 2017 +0100
@@ -267,17 +267,7 @@
   {
     val (reparse, perspective) = node_perspective(doc_blobs, hidden)
     if (reparse || pending_edits.nonEmpty || last_perspective != perspective) {
-      // FIXME eliminate clone
-      val edits: List[Document.Edit_Text] =
-        get_blob match {
-          case None =>
-            List(session.header_edit(node_name, node_header),
-              node_name -> Document.Node.Edits(pending_edits),
-              node_name -> perspective)
-          case Some(blob) =>
-            List(node_name -> Document.Node.Blob(blob),
-              node_name -> Document.Node.Edits(pending_edits))
-        }
+      val edits = node_edits(pending_edits, perspective)
       Some((edits, copy(last_perspective = perspective, pending_edits = Nil)))
     }
     else None
@@ -372,25 +362,6 @@
     }
 
 
-  /* edits */
-
-  def node_edits(text_edits: List[Text.Edit], perspective: Document.Node.Perspective_Text)
-    : List[Document.Edit_Text] =
-  {
-    val edits: List[Document.Edit_Text] =
-      get_blob match {
-        case None =>
-          List(session.header_edit(node_name, node_header()),
-            node_name -> Document.Node.Edits(text_edits),
-            node_name -> perspective)
-        case Some(blob) =>
-          List(node_name -> Document.Node.Blob(blob),
-            node_name -> Document.Node.Edits(text_edits))
-      }
-    edits.filterNot(_._2.is_void)
-  }
-
-
   /* pending edits */
 
   private object pending_edits