# HG changeset patch
# User wenzelm
# Date 1504190109 -7200
# Node ID 1e5ae735e026f615f8876aa22a86964e9b736e85
# Parent  0fdeb24e535e4248cd0d0ec330ed3c89017802aa
tolerate errors in session structure, although this may lead to confusion about theory imports later on;

diff -r 0fdeb24e535e -r 1e5ae735e026 src/Tools/jEdit/src/jedit_resources.scala
--- a/src/Tools/jEdit/src/jedit_resources.scala	Thu Aug 31 16:30:46 2017 +0200
+++ b/src/Tools/jEdit/src/jedit_resources.scala	Thu Aug 31 16:35:09 2017 +0200
@@ -21,7 +21,17 @@
 import org.gjt.sp.jedit.bufferio.BufferIORequest
 
 
-class JEdit_Resources(session_base: Sessions.Base) extends Resources(session_base)
+object JEdit_Resources
+{
+  def apply(options: Options): JEdit_Resources =
+  {
+    val (errs, base) = JEdit_Sessions.session_base(options)
+    new JEdit_Resources(errs, base)
+  }
+}
+
+class JEdit_Resources private(val session_errors: List[String], session_base: Sessions.Base)
+  extends Resources(session_base)
 {
   /* document node name */
 
diff -r 0fdeb24e535e -r 1e5ae735e026 src/Tools/jEdit/src/jedit_sessions.scala
--- a/src/Tools/jEdit/src/jedit_sessions.scala	Thu Aug 31 16:30:46 2017 +0200
+++ b/src/Tools/jEdit/src/jedit_sessions.scala	Thu Aug 31 16:35:09 2017 +0200
@@ -52,12 +52,13 @@
 
   def session_name(options: Options): String = session_info(options).name
 
-  def session_base(options: Options): Sessions.Base =
+  def session_base(options: Options): (List[String], Sessions.Base) =
   {
     val all_known = !session_restricted()
-    Sessions.session_base(
-      options, session_name(options), dirs = JEdit_Sessions.session_dirs(), all_known = all_known)
-    .platform_path
+    val (errs, base) =
+      Sessions.session_base_errors(
+        options, session_name(options), dirs = JEdit_Sessions.session_dirs(), all_known = all_known)
+    (errs, base.platform_path)
   }
 
   def session_build_mode(): String = Isabelle_System.getenv("JEDIT_BUILD_MODE")
diff -r 0fdeb24e535e -r 1e5ae735e026 src/Tools/jEdit/src/plugin.scala
--- a/src/Tools/jEdit/src/plugin.scala	Thu Aug 31 16:30:46 2017 +0200
+++ b/src/Tools/jEdit/src/plugin.scala	Thu Aug 31 16:35:09 2017 +0200
@@ -70,8 +70,7 @@
   /* resources */
 
   private var _resources: JEdit_Resources = null
-  private def init_resources(): Unit =
-    _resources = new JEdit_Resources(JEdit_Sessions.session_base(options.value))
+  private def init_resources(): Unit = _resources = JEdit_Resources(options.value)
   def resources: JEdit_Resources = _resources
 
 
@@ -311,6 +310,12 @@
               "It is for testing only, not for production use.")
           }
 
+          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)))
+          }
+
           val view = jEdit.getActiveView()
           init_view(view)