--- 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(())