--- a/src/Pure/PIDE/document.ML Sat Jan 10 22:04:43 2015 +0100
+++ b/src/Pure/PIDE/document.ML Sun Jan 11 12:46:19 2015 +0100
@@ -431,7 +431,7 @@
if visible_node node orelse pending_result node then
let
fun body () =
- if forall finished_import deps then
+ (if forall finished_import deps then
iterate_entries (fn (_, opt_exec) => fn () =>
(case opt_exec of
SOME exec =>
@@ -439,7 +439,8 @@
then SOME (Command.exec execution_id exec)
else NONE
| NONE => NONE)) node ()
- else ();
+ else ())
+ handle exn => (Output.system_message (Runtime.exn_message exn); reraise exn);
val future =
(singleton o Future.forks)
{name = "theory:" ^ name,