discontinue somewhat pointless thread tracing/debugging: without PIDE command context, messages are not shown, and Exn.trace hardly works anyway (see also de20fccf6509 and 447972249785);
prefer Isabelle_Thread.fork;
--- a/src/HOL/Tools/Sledgehammer/async_manager_legacy.ML Mon Sep 04 17:25:16 2023 +0200
+++ b/src/HOL/Tools/Sledgehammer/async_manager_legacy.ML Mon Sep 04 21:03:13 2023 +0200
@@ -19,13 +19,7 @@
struct
fun make_thread interrupts body =
- Thread.fork
- (fn () =>
- Runtime.debugging NONE body () handle exn =>
- if Exn.is_interrupt exn then ()
- else writeln ("## INTERNAL ERROR ##\n" ^ Runtime.exn_message exn),
- Isabelle_Thread.attributes
- {name = "async_manager", stack_limit = NONE, interrupts = interrupts});
+ Isabelle_Thread.fork {name = "async_manager", stack_limit = NONE, interrupts = interrupts} body;
fun implode_message (workers, work) =
space_implode " " (Try.serial_commas "and" workers) ^ work
--- a/src/Pure/Concurrent/isabelle_thread.ML Mon Sep 04 17:25:16 2023 +0200
+++ b/src/Pure/Concurrent/isabelle_thread.ML Mon Sep 04 21:03:13 2023 +0200
@@ -58,11 +58,7 @@
(if interrupts then Thread_Attributes.public_interrupts else Thread_Attributes.no_interrupts);
fun fork (params: params) body =
- Thread.fork (fn () =>
- Exn.trace General.exnMessage tracing (fn () =>
- (set_name (#name params); body ())
- handle exn => if Exn.is_interrupt exn then () (*sic!*) else Exn.reraise exn),
- attributes params);
+ Thread.fork (fn () => (set_name (#name params); body ()), attributes params);
(* join *)