# HG changeset patch
# User wenzelm
# Date 1392200897 -3600
# Node ID 662e0fd398236ae2e8e863f49351b97736424df0
# Parent  aa2918d967f07ef524bf89b682864844d03270f4
maintain blob edits within history, which is important for Snapshot.convert/revert;

diff -r aa2918d967f0 -r 662e0fd39823 src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Wed Feb 12 11:05:48 2014 +0100
+++ b/src/Pure/PIDE/document.scala	Wed Feb 12 11:28:17 2014 +0100
@@ -192,6 +192,7 @@
   }
 
   final class Node private(
+    val is_blob: Boolean = false,
     val header: Node.Header = Node.bad_header("Bad theory header"),
     val perspective: Node.Perspective_Command =
       Node.Perspective(false, Command.Perspective.empty, Node.Overlays.empty),
@@ -199,11 +200,13 @@
   {
     def clear: Node = new Node(header = header)
 
+    def init_blob: Node = new Node(is_blob = true)
+
     def update_header(new_header: Node.Header): Node =
-      new Node(new_header, perspective, _commands)
+      new Node(is_blob, new_header, perspective, _commands)
 
     def update_perspective(new_perspective: Node.Perspective_Command): Node =
-      new Node(header, new_perspective, _commands)
+      new Node(is_blob, header, new_perspective, _commands)
 
     def same_perspective(other_perspective: Node.Perspective_Command): Boolean =
       perspective.required == other_perspective.required &&
@@ -215,7 +218,7 @@
 
     def update_commands(new_commands: Linear_Set[Command]): Node =
       if (new_commands eq _commands.commands) this
-      else new Node(header, perspective, Node.Commands(new_commands))
+      else new Node(is_blob, header, perspective, Node.Commands(new_commands))
 
     def command_range(i: Text.Offset = 0): Iterator[(Command, Text.Offset)] =
       _commands.range(i)
diff -r aa2918d967f0 -r 662e0fd39823 src/Pure/Thy/thy_syntax.scala
--- a/src/Pure/Thy/thy_syntax.scala	Wed Feb 12 11:05:48 2014 +0100
+++ b/src/Pure/Thy/thy_syntax.scala	Wed Feb 12 11:28:17 2014 +0100
@@ -407,14 +407,17 @@
     edit match {
       case (_, Document.Node.Clear()) => node.clear
 
-      case (_, Document.Node.Blob()) => node
+      case (_, Document.Node.Blob()) => node.init_blob
 
       case (name, Document.Node.Edits(text_edits)) =>
-        val commands0 = node.commands
-        val commands1 = edit_text(text_edits, commands0)
-        val commands2 =
-          recover_spans(thy_load, syntax, doc_blobs, name, node.perspective.visible, commands1)
-        node.update_commands(commands2)
+        if (node.is_blob) node
+        else {
+          val commands0 = node.commands
+          val commands1 = edit_text(text_edits, commands0)
+          val commands2 =
+            recover_spans(thy_load, syntax, doc_blobs, name, node.perspective.visible, commands1)
+          node.update_commands(commands2)
+        }
 
       case (_, Document.Node.Deps(_)) => node
 
diff -r aa2918d967f0 -r 662e0fd39823 src/Tools/jEdit/src/document_model.scala
--- a/src/Tools/jEdit/src/document_model.scala	Wed Feb 12 11:05:48 2014 +0100
+++ b/src/Tools/jEdit/src/document_model.scala	Wed Feb 12 11:28:17 2014 +0100
@@ -167,7 +167,8 @@
         node_name -> Document.Node.Edits(List(Text.Edit.insert(0, text))),
         node_name -> perspective)
     else
-      List(node_name -> Document.Node.Blob())
+      List(node_name -> Document.Node.Blob(),
+        node_name -> Document.Node.Edits(List(Text.Edit.insert(0, text))))
   }
 
   def node_edits(
@@ -190,7 +191,8 @@
           node_name -> perspective)
     }
     else
-      List(node_name -> Document.Node.Blob())
+      List(node_name -> Document.Node.Blob(),
+        node_name -> Document.Node.Edits(text_edits))
   }