--- 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()