1.1 --- a/src/Pure/PIDE/command.ML	Wed Jul 03 22:30:33 2013 +0200
     1.2 +++ b/src/Pure/PIDE/command.ML	Wed Jul 03 23:02:00 2013 +0200
     1.3 @@ -165,14 +165,21 @@
     1.4  val print_functions =
     1.5    Synchronized.var "Command.print_functions" ([]: (string * (int * print_function)) list);
     1.6  
     1.7 +fun output_error tr exn =
     1.8 +  List.app (Future.error_msg (Toplevel.pos_of tr)) (ML_Compiler.exn_messages_ids exn);
     1.9 +
    1.10 +fun print_error tr f x =
    1.11 +  (Toplevel.setmp_thread_position tr o Runtime.controlled_execution) f x
    1.12 +    handle exn => output_error tr exn;
    1.13 +
    1.14  in
    1.15  
    1.16  fun print st tr st' =
    1.17    rev (Synchronized.value print_functions) |> map_filter (fn (name, (pri, f)) =>
    1.18 -    (case f {old_state = st, tr = tr, state = st'} of
    1.19 -      SOME pr =>
    1.20 -        SOME {name = name, pri = pri, pr = (Lazy.lazy o Toplevel.setmp_thread_position tr) pr}
    1.21 -    | NONE => NONE));
    1.22 +    (case Exn.capture (Runtime.controlled_execution f) {old_state = st, tr = tr, state = st'} of
    1.23 +      Exn.Res NONE => NONE
    1.24 +    | Exn.Res (SOME pr) => SOME {name = name, pri = pri, pr = (Lazy.lazy o print_error tr) pr}
    1.25 +    | Exn.Exn exn => SOME {name = name, pri = pri, pr = Lazy.lazy (fn () => output_error tr exn)}));
    1.26  
    1.27  fun print_function name pri f =
    1.28    Synchronized.change print_functions (fn funs =>