clarified fall-back base, e.g. relevant for "isabelle jedit -l BAD";
authorwenzelm
Wed, 15 Mar 2017 11:04:46 +0100
changeset 65254 3075aa3b40bf
parent 65253 85c0ac5c2589
child 65255 d388e63a46fc
clarified fall-back base, e.g. relevant for "isabelle jedit -l BAD";
src/Pure/Thy/sessions.scala
src/Tools/jEdit/src/jedit_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 */
 
--- 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(_))))
   }