# HG changeset patch
# User wenzelm
# Date 1671452409 -3600
# Node ID 2e231c07b4280c902dc25c7ea42fb127b369f44d
# Parent  3d4358e016467f828d74b55b0a64714d2dfe5d85
more informative errors, including optional Exn.trace;

diff -r 3d4358e01646 -r 2e231c07b428 src/Tools/jEdit/src/document_dockable.scala
--- a/src/Tools/jEdit/src/document_dockable.scala	Mon Dec 19 13:06:59 2022 +0100
+++ b/src/Tools/jEdit/src/document_dockable.scala	Mon Dec 19 13:20:09 2022 +0100
@@ -143,7 +143,7 @@
             }
             catch {
               case exn: Throwable if !Exn.is_interrupt(exn) =>
-                current_state.change(_.finish(Protocol.error_message(Exn.message(exn))))
+                current_state.change(_.finish(Protocol.error_message(Exn.print(exn))))
                 GUI_Thread.later { show_state(); show_page(output_page) }
             }
           }
@@ -175,7 +175,7 @@
             val msg =
               res match {
                 case Exn.Res(_) => Protocol.writeln_message("OK")
-                case Exn.Exn(exn) => Protocol.error_message(Exn.message(exn))
+                case Exn.Exn(exn) => Protocol.error_message(Exn.print(exn))
               }
             current_state.change(_.finish(msg))
             show_state()