# 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);