# HG changeset patch
# User wenzelm
# Date 1279649427 -7200
# Node ID 4e4b8c0dc76627f1ddc6430d8b2d9f1a28bf12c0
# Parent  173974e07dea2411d977504506539766785fb845
execute document version at high priority;

diff -r 173974e07dea -r 4e4b8c0dc766 src/Pure/Isar/isar_document.ML
--- a/src/Pure/Isar/isar_document.ML	Tue Jul 20 18:33:19 2010 +0200
+++ b/src/Pure/Isar/isar_document.ML	Tue Jul 20 20:10:27 2010 +0200
@@ -241,7 +241,7 @@
     let
       val old_execution = ! execution;
       val _ = Future.cancel old_execution;
-      val new_execution = Future.fork (fn () =>
+      val new_execution = Future.fork_pri 1 (fn () =>
        (uninterruptible (K Future.join_result) old_execution;
         fold_entries no_id (fn (_, {state, ...}) => fn () => force_state state) document ()));
     in execution := new_execution end);