# HG changeset patch
# User wenzelm
# Date 1489572286 -3600
# Node ID 3075aa3b40bf3ca97955789cb6c530454b6164c1
# Parent  85c0ac5c2589405d3fc2a3dd8879d00ab78c7524
clarified fall-back base, e.g. relevant for "isabelle jedit -l BAD";

diff -r 85c0ac5c2589 -r 3075aa3b40bf src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Wed Mar 15 10:48:46 2017 +0100
+++ b/src/Pure/Thy/sessions.scala	Wed Mar 15 11:04:46 2017 +0100
@@ -28,6 +28,8 @@
     (roots ::: loaded_files).map(file => dir + Path.explode(file))
   }
 
+  def pure_base(options: Options): Base = session_base(options, Thy_Header.PURE)
+
 
   /* base info and source dependencies */
 
diff -r 85c0ac5c2589 -r 3075aa3b40bf src/Tools/jEdit/src/jedit_sessions.scala
--- a/src/Tools/jEdit/src/jedit_sessions.scala	Wed Mar 15 10:48:46 2017 +0100
+++ b/src/Tools/jEdit/src/jedit_sessions.scala	Wed Mar 15 11:04:46 2017 +0100
@@ -83,7 +83,7 @@
   {
     val base =
       try { Sessions.session_base(PIDE.options.value, session_name(), session_dirs()) }
-      catch { case ERROR(_) => Sessions.Base.empty }
+      catch { case ERROR(_) => Sessions.pure_base(PIDE.options.value) }
     base.copy(known_theories =
       for ((a, b) <- base.known_theories) yield (a, b.map(File.platform_path(_))))
   }