changeset 41629 | 5490dc4d999d |
parent 41537 | 3837045cc8a1 |
child 41630 | a7a93df23664 |
--- a/src/Pure/PIDE/document.ML Mon Jan 24 21:30:33 2011 +0100 +++ b/src/Pure/PIDE/document.ML Tue Jan 25 20:06:32 2011 +0100 @@ -284,6 +284,7 @@ fun edit (old_id: version_id) (new_id: version_id) edits state = let val old_version = the_version state old_id; + val _ = Time.now (); (* FIXME odd workaround *) val new_version = fold edit_nodes edits old_version; fun update_node name (rev_updates, version, st) =