# HG changeset patch
# User wenzelm
# Date 1279642790 -7200
# Node ID 1ad8205078d429c3841850a392ae72aa3422277d
# Parent  047c96f414554023ea4645e178d997320f466cd7
edit_document: join parent execution in synchronous/uninterruptible mode, to prevent spurious interrupts when cascaded executions run into each other;

diff -r 047c96f41455 -r 1ad8205078d4 src/Pure/Isar/isar_document.ML
--- a/src/Pure/Isar/isar_document.ML	Tue Jul 20 17:35:42 2010 +0200
+++ b/src/Pure/Isar/isar_document.ML	Tue Jul 20 18:19:50 2010 +0200
@@ -242,7 +242,7 @@
       val old_execution = ! execution;
       val _ = Future.cancel old_execution;
       val new_execution = Future.fork (fn () =>
-       (Future.join_result old_execution;
+       (uninterruptible (K Future.join_result) old_execution;
         fold_entries no_id (fn (_, {state, ...}) => fn () => force_state state) document ()));
     in execution := new_execution end);