more elementary exception handling: evade hard crash of (Runtime.thread true undefined) on Poly/ML 5.5.1 and 5.5.2;
--- a/src/Pure/Isar/runtime.ML Thu Jul 24 20:21:59 2014 +0200
+++ b/src/Pure/Isar/runtime.ML Thu Jul 24 23:17:26 2014 +0200
@@ -166,10 +166,10 @@
(*Proof General legacy*)
fun thread interrupts body =
Thread.fork
- (((fn () => body () handle exn => if Exn.is_interrupt exn then () else reraise exn)
- |> debugging NONE
- |> toplevel_error
- (fn exn => Output.urgent_message ("## INTERNAL ERROR ##\n" ^ exn_message exn))),
+ (fn () =>
+ debugging NONE body () handle exn =>
+ if Exn.is_interrupt exn then ()
+ else Output.urgent_message ("## INTERNAL ERROR ##\n" ^ exn_message exn),
Simple_Thread.attributes interrupts);
end;