maintain blob edits within history, which is important for Snapshot.convert/revert;
--- 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)
--- 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
--- 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))
}