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);
authorwenzelm
Mon, 04 Sep 2023 21:03:13 +0200
changeset 78647 27380538d632
parent 78646 fff610f1a6f4
child 78648 852ec09aef13
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;
src/HOL/Tools/Sledgehammer/async_manager_legacy.ML
src/Pure/Concurrent/isabelle_thread.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
--- 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 *)