# HG changeset patch
# User wenzelm
# Date 1717868128 -7200
# Node ID 152d6c58adb3d15914997e9cc6814bd7f3a2cc4c
# Parent  a397fd0c451ae2dc9d51920309eb4bddb953e2b4
more informative exception output, with optional trace;

diff -r a397fd0c451a -r 152d6c58adb3 src/Pure/Concurrent/consumer_thread.scala
--- a/src/Pure/Concurrent/consumer_thread.scala	Sat Jun 08 16:26:47 2024 +0200
+++ b/src/Pure/Concurrent/consumer_thread.scala	Sat Jun 08 19:35:28 2024 +0200
@@ -57,7 +57,7 @@
 
   private def failure(exn: Throwable): Unit =
     Output.error_message(
-      "Consumer thread failure: " + quote(thread.getName) + "\n" + Exn.message(exn))
+      "Consumer thread failure: " + quote(thread.getName) + "\n" + Exn.print(exn))
 
   private def robust_finish(): Unit =
     try { finish() } catch { case exn: Throwable => failure(exn) }
diff -r a397fd0c451a -r 152d6c58adb3 src/Pure/PIDE/protocol_handlers.scala
--- a/src/Pure/PIDE/protocol_handlers.scala	Sat Jun 08 16:26:47 2024 +0200
+++ b/src/Pure/PIDE/protocol_handlers.scala	Sat Jun 08 19:35:28 2024 +0200
@@ -9,7 +9,7 @@
 
 object Protocol_Handlers {
   private def err_handler(exn: Throwable, name: String): Nothing =
-    error("Failed to initialize protocol handler: " + quote(name) + "\n" + Exn.message(exn))
+    error("Failed to initialize protocol handler: " + quote(name) + "\n" + Exn.print(exn))
 
   sealed case class State(
     session: Session,
@@ -49,7 +49,7 @@
           catch {
             case exn: Throwable =>
               Output.error_message(
-                "Failed invocation of protocol function: " + quote(a) + "\n" + Exn.message(exn))
+                "Failed invocation of protocol function: " + quote(a) + "\n" + Exn.print(exn))
             false
           }
         case _ => false
diff -r a397fd0c451a -r 152d6c58adb3 src/Pure/PIDE/session.scala
--- a/src/Pure/PIDE/session.scala	Sat Jun 08 16:26:47 2024 +0200
+++ b/src/Pure/PIDE/session.scala	Sat Jun 08 19:35:28 2024 +0200
@@ -34,7 +34,7 @@
           try { c.consume(a) }
           catch {
             case exn: Throwable =>
-              Output.error_message("Consumer failed: " + quote(c.name) + "\n" + Exn.message(exn))
+              Output.error_message("Consumer failed: " + quote(c.name) + "\n" + Exn.print(exn))
           })
       }
     }
diff -r a397fd0c451a -r 152d6c58adb3 src/Pure/System/classpath.scala
--- a/src/Pure/System/classpath.scala	Sat Jun 08 16:26:47 2024 +0200
+++ b/src/Pure/System/classpath.scala	Sat Jun 08 19:35:28 2024 +0200
@@ -74,7 +74,7 @@
       try { Class.forName(name, true, class_loader).asInstanceOf[Classpath.Service_Class] }
       catch {
         case _: ClassNotFoundException => err("Class not found")
-        case exn: Throwable => err(Exn.message(exn))
+        case exn: Throwable => err(Exn.print(exn))
       }
     }
   }