clarified fall-back base, e.g. relevant for "isabelle jedit -l BAD";
--- 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(_))))
}