proper update of perspective after implicit edit due to reparse (e.g. ~~/src/HOL/Nat.thy);

--- a/src/Pure/PIDE/document.scala	Thu Jan 15 16:26:23 2015 +0100
+++ b/src/Pure/PIDE/document.scala	Thu Jan 15 20:36:26 2015 +0100
@@ -245,12 +245,14 @@
     val get_blob: Option[Document.Blob] = None,
     val header: Node.Header = Node.no_header,
     val syntax: Option[Prover.Syntax] = None,
+    val text_perspective: Text.Perspective = Text.Perspective.empty,
     val perspective: Node.Perspective_Command = Node.no_perspective_command,
     _commands: Node.Commands = Node.Commands.empty)
   {
     def is_empty: Boolean =
       get_blob.isEmpty &&
       header == Node.no_header &&
+      text_perspective.is_empty &&
       Node.is_no_perspective_command(perspective) &&
       commands.isEmpty
 
@@ -262,22 +264,32 @@
     def init_blob(blob: Document.Blob): Node = new Node(get_blob = Some(blob.unchanged))
 
     def update_header(new_header: Node.Header): Node =
-      new Node(get_blob, new_header, syntax, perspective, _commands)
+      new Node(get_blob, new_header, syntax, text_perspective, perspective, _commands)
 
     def update_syntax(new_syntax: Option[Prover.Syntax]): Node =
-      new Node(get_blob, header, new_syntax, perspective, _commands)
+      new Node(get_blob, header, new_syntax, text_perspective, perspective, _commands)
+
+    def update_perspective(
+        new_text_perspective: Text.Perspective,
+        new_perspective: Node.Perspective_Command): Node =
+      new Node(get_blob, header, syntax, new_text_perspective, new_perspective, _commands)
 
-    def update_perspective(new_perspective: Node.Perspective_Command): Node =
-      new Node(get_blob, header, syntax, new_perspective, _commands)
+    def edit_perspective: Node.Edit[Text.Edit, Text.Perspective] =
+      Node.Perspective(perspective.required, text_perspective, perspective.overlays)
 
-    def same_perspective(other_perspective: Node.Perspective_Command): Boolean =
+    def same_perspective(
+        other_text_perspective: Text.Perspective,
+        other_perspective: Node.Perspective_Command): Boolean =
+      text_perspective == other_text_perspective &&
       perspective.required == other_perspective.required &&
       perspective.visible.same(other_perspective.visible) &&
       perspective.overlays == other_perspective.overlays
 
     def update_commands(new_commands: Linear_Set[Command]): Node =
       if (new_commands eq _commands.commands) this
-      else new Node(get_blob, header, syntax, perspective, Node.Commands(new_commands))
+      else
+        new Node(get_blob, header, syntax, text_perspective, perspective,
+          Node.Commands(new_commands))
 
     def command_iterator(i: Text.Offset = 0): Iterator[(Command, Text.Offset)] =
       _commands.iterator(i)

--- a/src/Pure/Thy/thy_syntax.scala	Thu Jan 15 16:26:23 2015 +0100
+++ b/src/Pure/Thy/thy_syntax.scala	Thu Jan 15 20:36:26 2015 +0100
@@ -288,11 +288,12 @@
         val (visible, visible_overlay) = command_perspective(node, text_perspective, overlays)
         val perspective: Document.Node.Perspective_Command =
           Document.Node.Perspective(required, visible_overlay, overlays)
-        if (node.same_perspective(perspective)) node
+        if (node.same_perspective(text_perspective, perspective)) node
         else
-          node.update_perspective(perspective).update_commands(
-            consolidate_spans(resources, syntax, get_blob, reparse_limit,
-              name, visible, node.commands))
+          node.update_perspective(text_perspective, perspective).
+            update_commands(
+              consolidate_spans(resources, syntax, get_blob, reparse_limit,
+                name, visible, node.commands))
     }
   }
 
@@ -341,13 +342,18 @@
               else node
             val node2 =
               (node1 /: edits)(text_edit(resources, syntax, get_blob, reparse_limit, _, _))
-
-            if (!(node.same_perspective(node2.perspective)))
-              doc_edits += (name -> node2.perspective)
+            val node3 =
+              if (reparse_set.contains(name))
+                text_edit(resources, syntax, get_blob, reparse_limit,
+                  node2, (name, node2.edit_perspective))
+              else node2
 
-            doc_edits += (name -> Document.Node.Edits(diff_commands(commands, node2.commands)))
+            if (!(node.same_perspective(node3.text_perspective, node3.perspective)))
+              doc_edits += (name -> node3.perspective)
 
-            nodes += (name -> node2)
+            doc_edits += (name -> Document.Node.Edits(diff_commands(commands, node3.commands)))
+
+            nodes += (name -> node3)
         }
         (doc_edits.toList.filterNot(_._2.is_void), Document.Version.make(nodes))
       }