# HG changeset patch
# User wenzelm
# Date 1693854193 -7200
# Node ID 27380538d632c91120368af834e4fc3364b49ca9
# Parent  fff610f1a6f4069382e223be58b4090695408f56
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;

diff -r fff610f1a6f4 -r 27380538d632 src/HOL/Tools/Sledgehammer/async_manager_legacy.ML
--- 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
diff -r fff610f1a6f4 -r 27380538d632 src/Pure/Concurrent/isabelle_thread.ML
--- 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 *)