maintain blob edits within history, which is important for Snapshot.convert/revert;
authorwenzelm
Wed Feb 12 11:28:17 2014 +0100 (2014-02-12)
changeset 55435662e0fd39823
parent 55434 aa2918d967f0
child 55436 9781e17dcc23
maintain blob edits within history, which is important for Snapshot.convert/revert;
src/Pure/PIDE/document.scala
src/Pure/Thy/thy_syntax.scala
src/Tools/jEdit/src/document_model.scala
     1.1 --- a/src/Pure/PIDE/document.scala	Wed Feb 12 11:05:48 2014 +0100
     1.2 +++ b/src/Pure/PIDE/document.scala	Wed Feb 12 11:28:17 2014 +0100
     1.3 @@ -192,6 +192,7 @@
     1.4    }
     1.5  
     1.6    final class Node private(
     1.7 +    val is_blob: Boolean = false,
     1.8      val header: Node.Header = Node.bad_header("Bad theory header"),
     1.9      val perspective: Node.Perspective_Command =
    1.10        Node.Perspective(false, Command.Perspective.empty, Node.Overlays.empty),
    1.11 @@ -199,11 +200,13 @@
    1.12    {
    1.13      def clear: Node = new Node(header = header)
    1.14  
    1.15 +    def init_blob: Node = new Node(is_blob = true)
    1.16 +
    1.17      def update_header(new_header: Node.Header): Node =
    1.18 -      new Node(new_header, perspective, _commands)
    1.19 +      new Node(is_blob, new_header, perspective, _commands)
    1.20  
    1.21      def update_perspective(new_perspective: Node.Perspective_Command): Node =
    1.22 -      new Node(header, new_perspective, _commands)
    1.23 +      new Node(is_blob, header, new_perspective, _commands)
    1.24  
    1.25      def same_perspective(other_perspective: Node.Perspective_Command): Boolean =
    1.26        perspective.required == other_perspective.required &&
    1.27 @@ -215,7 +218,7 @@
    1.28  
    1.29      def update_commands(new_commands: Linear_Set[Command]): Node =
    1.30        if (new_commands eq _commands.commands) this
    1.31 -      else new Node(header, perspective, Node.Commands(new_commands))
    1.32 +      else new Node(is_blob, header, perspective, Node.Commands(new_commands))
    1.33  
    1.34      def command_range(i: Text.Offset = 0): Iterator[(Command, Text.Offset)] =
    1.35        _commands.range(i)
     2.1 --- a/src/Pure/Thy/thy_syntax.scala	Wed Feb 12 11:05:48 2014 +0100
     2.2 +++ b/src/Pure/Thy/thy_syntax.scala	Wed Feb 12 11:28:17 2014 +0100
     2.3 @@ -407,14 +407,17 @@
     2.4      edit match {
     2.5        case (_, Document.Node.Clear()) => node.clear
     2.6  
     2.7 -      case (_, Document.Node.Blob()) => node
     2.8 +      case (_, Document.Node.Blob()) => node.init_blob
     2.9  
    2.10        case (name, Document.Node.Edits(text_edits)) =>
    2.11 -        val commands0 = node.commands
    2.12 -        val commands1 = edit_text(text_edits, commands0)
    2.13 -        val commands2 =
    2.14 -          recover_spans(thy_load, syntax, doc_blobs, name, node.perspective.visible, commands1)
    2.15 -        node.update_commands(commands2)
    2.16 +        if (node.is_blob) node
    2.17 +        else {
    2.18 +          val commands0 = node.commands
    2.19 +          val commands1 = edit_text(text_edits, commands0)
    2.20 +          val commands2 =
    2.21 +            recover_spans(thy_load, syntax, doc_blobs, name, node.perspective.visible, commands1)
    2.22 +          node.update_commands(commands2)
    2.23 +        }
    2.24  
    2.25        case (_, Document.Node.Deps(_)) => node
    2.26  
     3.1 --- a/src/Tools/jEdit/src/document_model.scala	Wed Feb 12 11:05:48 2014 +0100
     3.2 +++ b/src/Tools/jEdit/src/document_model.scala	Wed Feb 12 11:28:17 2014 +0100
     3.3 @@ -167,7 +167,8 @@
     3.4          node_name -> Document.Node.Edits(List(Text.Edit.insert(0, text))),
     3.5          node_name -> perspective)
     3.6      else
     3.7 -      List(node_name -> Document.Node.Blob())
     3.8 +      List(node_name -> Document.Node.Blob(),
     3.9 +        node_name -> Document.Node.Edits(List(Text.Edit.insert(0, text))))
    3.10    }
    3.11  
    3.12    def node_edits(
    3.13 @@ -190,7 +191,8 @@
    3.14            node_name -> perspective)
    3.15      }
    3.16      else
    3.17 -      List(node_name -> Document.Node.Blob())
    3.18 +      List(node_name -> Document.Node.Blob(),
    3.19 +        node_name -> Document.Node.Edits(text_edits))
    3.20    }
    3.21  
    3.22