more explicit errors;
authorwenzelm
Sun Jan 11 12:46:19 2015 +0100 (2015-01-11)
changeset 593472183c731f0a7
parent 59346 f25442e194bf
child 59348 8a6788917b32
more explicit errors;
src/Pure/PIDE/document.ML
     1.1 --- a/src/Pure/PIDE/document.ML	Sat Jan 10 22:04:43 2015 +0100
     1.2 +++ b/src/Pure/PIDE/document.ML	Sun Jan 11 12:46:19 2015 +0100
     1.3 @@ -431,7 +431,7 @@
     1.4              if visible_node node orelse pending_result node then
     1.5                let
     1.6                  fun body () =
     1.7 -                  if forall finished_import deps then
     1.8 +                  (if forall finished_import deps then
     1.9                      iterate_entries (fn (_, opt_exec) => fn () =>
    1.10                        (case opt_exec of
    1.11                          SOME exec =>
    1.12 @@ -439,7 +439,8 @@
    1.13                            then SOME (Command.exec execution_id exec)
    1.14                            else NONE
    1.15                        | NONE => NONE)) node ()
    1.16 -                  else ();
    1.17 +                   else ())
    1.18 +                   handle exn => (Output.system_message (Runtime.exn_message exn); reraise exn);
    1.19                  val future =
    1.20                    (singleton o Future.forks)
    1.21                     {name = "theory:" ^ name,