# HG changeset patch
# User wenzelm
# Date 1666278306 -7200
# Node ID adb3f8d33838e73e5ee8a253c3cff8df21bdd7ef
# Parent  6a6f650cc5a214654daf5a552c65e8ec0de4ddcd
more informative errors, with optional exception trace as in Command_Line.tool;

diff -r 6a6f650cc5a2 -r adb3f8d33838 src/Tools/jEdit/src/jedit_main.scala
--- a/src/Tools/jEdit/src/jedit_main.scala	Thu Oct 20 14:59:39 2022 +0200
+++ b/src/Tools/jEdit/src/jedit_main.scala	Thu Oct 20 17:05:06 2022 +0200
@@ -128,7 +128,7 @@
         catch {
           case exn: Throwable =>
             GUI.init_laf()
-            GUI.dialog(null, "Isabelle", GUI.scrollable_text(Exn.message(exn)))
+            GUI.dialog(null, "Isabelle main", GUI.scrollable_text(Exn.print(exn)))
             sys.exit(Process_Result.RC.failure)
         }
       }
diff -r 6a6f650cc5a2 -r adb3f8d33838 src/Tools/jEdit/src/session_build.scala
--- a/src/Tools/jEdit/src/session_build.scala	Thu Oct 20 14:59:39 2022 +0200
+++ b/src/Tools/jEdit/src/session_build.scala	Thu Oct 20 17:05:06 2022 +0200
@@ -29,7 +29,7 @@
       }
       catch {
         case exn: Throwable =>
-          GUI.dialog(view, "Isabelle", GUI.scrollable_text(Exn.message(exn)))
+          GUI.dialog(view, "Isabelle build", GUI.scrollable_text(Exn.print(exn)))
       }
     }
   }