# HG changeset patch
# User wenzelm
# Date 1314389652 -7200
# Node ID 470f2ee5950e6307abc86d694463bbc6c571a7e9
# Parent  383a5b9efbd02da2454c289acebf3b5b38a6ebe1
tuned Session.edit_node: update_perspective based on last_exec_offset;

diff -r 383a5b9efbd0 -r 470f2ee5950e src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Fri Aug 26 21:27:58 2011 +0200
+++ b/src/Pure/PIDE/document.scala	Fri Aug 26 22:14:12 2011 +0200
@@ -322,6 +322,21 @@
     def tip_stable: Boolean = is_stable(history.tip)
     def tip_version: Version = history.tip.version.get_finished
 
+    def last_exec_offset(name: String): Text.Offset =
+    {
+      val version = tip_version
+      the_assignment(version).last_execs.get(name) match {
+        case Some(Some(id)) =>
+          val node = version.nodes(name)
+          val cmd = the_command(id).command
+          node.command_start(cmd) match {
+            case None => 0
+            case Some(start) => start + cmd.length
+          }
+        case _ => 0
+      }
+    }
+
     def continue_history(
         previous: Future[Version],
         edits: List[Edit_Text],
diff -r 383a5b9efbd0 -r 470f2ee5950e src/Pure/System/session.scala
--- a/src/Pure/System/session.scala	Fri Aug 26 21:27:58 2011 +0200
+++ b/src/Pure/System/session.scala	Fri Aug 26 22:14:12 2011 +0200
@@ -380,10 +380,10 @@
           reply(())
 
         case Edit_Node(name, master_dir, header, perspective, text_edits) if prover.isDefined =>
-// FIXME
-//          if (text_edits.isEmpty && global_state().tip_stable)
-//            update_perspective(name, perspective)
-//          else
+          if (text_edits.isEmpty && global_state().tip_stable &&
+              perspective.range.stop <= global_state().last_exec_offset(name))
+            update_perspective(name, perspective)
+          else
             handle_edits(name, master_dir, header,
               List(Document.Node.Edits(text_edits), Document.Node.Perspective(perspective)))
           reply(())