# HG changeset patch
# User wenzelm
# Date 1671292929 -3600
# Node ID 981801179bc50819f51f8c5e6c0858e56a18d5c0
# Parent  7530d49d928af4af218cc7ce73cd0f828476acb0
clarified signature;

diff -r 7530d49d928a -r 981801179bc5 src/Pure/PIDE/resources.scala
--- a/src/Pure/PIDE/resources.scala	Sat Dec 17 16:41:54 2022 +0100
+++ b/src/Pure/PIDE/resources.scala	Sat Dec 17 17:02:09 2022 +0100
@@ -31,7 +31,6 @@
 
   def sessions_structure: Sessions.Structure = session_background.sessions_structure
   def session_base: Sessions.Base = session_background.base
-  def session_errors: List[String] = session_background.errors
 
   override def toString: String = "Resources(" + session_base.print_body + ")"
 
diff -r 7530d49d928a -r 981801179bc5 src/Tools/jEdit/src/main_plugin.scala
--- a/src/Tools/jEdit/src/main_plugin.scala	Sat Dec 17 16:41:54 2022 +0100
+++ b/src/Tools/jEdit/src/main_plugin.scala	Sat Dec 17 17:02:09 2022 +0100
@@ -298,10 +298,12 @@
     if (startup_failure.isEmpty) {
       message match {
         case _: EditorStarted =>
-          if (resources.session_errors.nonEmpty) {
-            GUI.warning_dialog(jEdit.getActiveView,
-              "Bad session structure: may cause problems with theory imports",
-              GUI.scrollable_text(cat_lines(resources.session_errors)))
+          try { resources.session_background.check_errors }
+          catch {
+            case ERROR(msg) =>
+              GUI.warning_dialog(jEdit.getActiveView,
+                "Bad session structure: may cause problems with theory imports",
+                GUI.scrollable_text(msg))
           }
 
           jEdit.propertiesChanged()