# 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 *)