src/Pure/PIDE/document.scala
changeset 55435 662e0fd39823
parent 55434 aa2918d967f0
child 55620 19dffae33cde
     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)