# HG changeset patch
# User wenzelm
# Date 1372885320 -7200
# Node ID b5b3c888df9f98952d726c3a2cd56cf8f7795d13
# Parent  0dcadc90550b42ec6a3a800dd01b4ae77ee33939
more exception handling -- make print functions total;

diff -r 0dcadc90550b -r b5b3c888df9f src/Pure/PIDE/command.ML
--- a/src/Pure/PIDE/command.ML	Wed Jul 03 22:30:33 2013 +0200
+++ b/src/Pure/PIDE/command.ML	Wed Jul 03 23:02:00 2013 +0200
@@ -165,14 +165,21 @@
 val print_functions =
   Synchronized.var "Command.print_functions" ([]: (string * (int * print_function)) list);
 
+fun output_error tr exn =
+  List.app (Future.error_msg (Toplevel.pos_of tr)) (ML_Compiler.exn_messages_ids exn);
+
+fun print_error tr f x =
+  (Toplevel.setmp_thread_position tr o Runtime.controlled_execution) f x
+    handle exn => output_error tr exn;
+
 in
 
 fun print st tr st' =
   rev (Synchronized.value print_functions) |> map_filter (fn (name, (pri, f)) =>
-    (case f {old_state = st, tr = tr, state = st'} of
-      SOME pr =>
-        SOME {name = name, pri = pri, pr = (Lazy.lazy o Toplevel.setmp_thread_position tr) pr}
-    | NONE => NONE));
+    (case Exn.capture (Runtime.controlled_execution f) {old_state = st, tr = tr, state = st'} of
+      Exn.Res NONE => NONE
+    | Exn.Res (SOME pr) => SOME {name = name, pri = pri, pr = (Lazy.lazy o print_error tr) pr}
+    | Exn.Exn exn => SOME {name = name, pri = pri, pr = Lazy.lazy (fn () => output_error tr exn)}));
 
 fun print_function name pri f =
   Synchronized.change print_functions (fn funs =>