proper update of perspective after implicit edit due to reparse (e.g. ~~/src/HOL/Nat.thy);
authorwenzelm
Thu Jan 15 20:36:26 2015 +0100 (2015-01-15)
changeset 59372503739360344
parent 59371 30b8e4ff0379
child 59373 6162878e3e53
proper update of perspective after implicit edit due to reparse (e.g. ~~/src/HOL/Nat.thy);
src/Pure/PIDE/document.scala
src/Pure/Thy/thy_syntax.scala
     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)
     2.1 --- a/src/Pure/Thy/thy_syntax.scala	Thu Jan 15 16:26:23 2015 +0100
     2.2 +++ b/src/Pure/Thy/thy_syntax.scala	Thu Jan 15 20:36:26 2015 +0100
     2.3 @@ -288,11 +288,12 @@
     2.4          val (visible, visible_overlay) = command_perspective(node, text_perspective, overlays)
     2.5          val perspective: Document.Node.Perspective_Command =
     2.6            Document.Node.Perspective(required, visible_overlay, overlays)
     2.7 -        if (node.same_perspective(perspective)) node
     2.8 +        if (node.same_perspective(text_perspective, perspective)) node
     2.9          else
    2.10 -          node.update_perspective(perspective).update_commands(
    2.11 -            consolidate_spans(resources, syntax, get_blob, reparse_limit,
    2.12 -              name, visible, node.commands))
    2.13 +          node.update_perspective(text_perspective, perspective).
    2.14 +            update_commands(
    2.15 +              consolidate_spans(resources, syntax, get_blob, reparse_limit,
    2.16 +                name, visible, node.commands))
    2.17      }
    2.18    }
    2.19  
    2.20 @@ -341,13 +342,18 @@
    2.21                else node
    2.22              val node2 =
    2.23                (node1 /: edits)(text_edit(resources, syntax, get_blob, reparse_limit, _, _))
    2.24 -
    2.25 -            if (!(node.same_perspective(node2.perspective)))
    2.26 -              doc_edits += (name -> node2.perspective)
    2.27 +            val node3 =
    2.28 +              if (reparse_set.contains(name))
    2.29 +                text_edit(resources, syntax, get_blob, reparse_limit,
    2.30 +                  node2, (name, node2.edit_perspective))
    2.31 +              else node2
    2.32  
    2.33 -            doc_edits += (name -> Document.Node.Edits(diff_commands(commands, node2.commands)))
    2.34 +            if (!(node.same_perspective(node3.text_perspective, node3.perspective)))
    2.35 +              doc_edits += (name -> node3.perspective)
    2.36  
    2.37 -            nodes += (name -> node2)
    2.38 +            doc_edits += (name -> Document.Node.Edits(diff_commands(commands, node3.commands)))
    2.39 +
    2.40 +            nodes += (name -> node3)
    2.41          }
    2.42          (doc_edits.toList.filterNot(_._2.is_void), Document.Version.make(nodes))
    2.43        }