clarified signature;
authorwenzelm
Sat, 17 Dec 2022 17:02:09 +0100
changeset 76666 981801179bc5
parent 76665 7530d49d928a
child 76667 fa81f218c96e
clarified signature;
src/Pure/PIDE/resources.scala
src/Tools/jEdit/src/main_plugin.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 + ")"
 
--- 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()