avoid application crash due to wrong requirement -- result is joined, but change not necessarily finished due to extra map;
authorwenzelm
Sat, 28 Aug 2010 17:37:57 +0200
changeset 38842 f762b33e0821
parent 38841 4df7b76249a0
child 38843 d95522496593
avoid application crash due to wrong requirement -- result is joined, but change not necessarily finished due to extra map;
src/Pure/System/session.scala
--- a/src/Pure/System/session.scala	Sat Aug 28 17:27:38 2010 +0200
+++ b/src/Pure/System/session.scala	Sat Aug 28 17:37:57 2010 +0200
@@ -126,8 +126,6 @@
     def handle_change(change: Document.Change)
     //{{{
     {
-      require(change.is_finished)
-
       val previous = change.previous.join
       val (node_edits, current) = change.result.join