src/Pure/PIDE/document.scala
changeset 59372 503739360344
parent 59319 677615cba30d
child 59695 a03e0561bdbf
     1.1 --- a/src/Pure/PIDE/document.scala	Thu Jan 15 16:26:23 2015 +0100
     1.2 +++ b/src/Pure/PIDE/document.scala	Thu Jan 15 20:36:26 2015 +0100
     1.3 @@ -245,12 +245,14 @@
     1.4      val get_blob: Option[Document.Blob] = None,
     1.5      val header: Node.Header = Node.no_header,
     1.6      val syntax: Option[Prover.Syntax] = None,
     1.7 +    val text_perspective: Text.Perspective = Text.Perspective.empty,
     1.8      val perspective: Node.Perspective_Command = Node.no_perspective_command,
     1.9      _commands: Node.Commands = Node.Commands.empty)
    1.10    {
    1.11      def is_empty: Boolean =
    1.12        get_blob.isEmpty &&
    1.13        header == Node.no_header &&
    1.14 +      text_perspective.is_empty &&
    1.15        Node.is_no_perspective_command(perspective) &&
    1.16        commands.isEmpty
    1.17  
    1.18 @@ -262,22 +264,32 @@
    1.19      def init_blob(blob: Document.Blob): Node = new Node(get_blob = Some(blob.unchanged))
    1.20  
    1.21      def update_header(new_header: Node.Header): Node =
    1.22 -      new Node(get_blob, new_header, syntax, perspective, _commands)
    1.23 +      new Node(get_blob, new_header, syntax, text_perspective, perspective, _commands)
    1.24  
    1.25      def update_syntax(new_syntax: Option[Prover.Syntax]): Node =
    1.26 -      new Node(get_blob, header, new_syntax, perspective, _commands)
    1.27 +      new Node(get_blob, header, new_syntax, text_perspective, perspective, _commands)
    1.28 +
    1.29 +    def update_perspective(
    1.30 +        new_text_perspective: Text.Perspective,
    1.31 +        new_perspective: Node.Perspective_Command): Node =
    1.32 +      new Node(get_blob, header, syntax, new_text_perspective, new_perspective, _commands)
    1.33  
    1.34 -    def update_perspective(new_perspective: Node.Perspective_Command): Node =
    1.35 -      new Node(get_blob, header, syntax, new_perspective, _commands)
    1.36 +    def edit_perspective: Node.Edit[Text.Edit, Text.Perspective] =
    1.37 +      Node.Perspective(perspective.required, text_perspective, perspective.overlays)
    1.38  
    1.39 -    def same_perspective(other_perspective: Node.Perspective_Command): Boolean =
    1.40 +    def same_perspective(
    1.41 +        other_text_perspective: Text.Perspective,
    1.42 +        other_perspective: Node.Perspective_Command): Boolean =
    1.43 +      text_perspective == other_text_perspective &&
    1.44        perspective.required == other_perspective.required &&
    1.45        perspective.visible.same(other_perspective.visible) &&
    1.46        perspective.overlays == other_perspective.overlays
    1.47  
    1.48      def update_commands(new_commands: Linear_Set[Command]): Node =
    1.49        if (new_commands eq _commands.commands) this
    1.50 -      else new Node(get_blob, header, syntax, perspective, Node.Commands(new_commands))
    1.51 +      else
    1.52 +        new Node(get_blob, header, syntax, text_perspective, perspective,
    1.53 +          Node.Commands(new_commands))
    1.54  
    1.55      def command_iterator(i: Text.Offset = 0): Iterator[(Command, Text.Offset)] =
    1.56        _commands.iterator(i)