--- a/src/Pure/Thy/sessions.scala Tue Oct 31 18:45:33 2017 +0100
+++ b/src/Pure/Thy/sessions.scala Tue Oct 31 18:56:24 2017 +0100
@@ -336,12 +336,13 @@
val deps = Sessions.deps(sessions, global_theories, inlined_files = inlined_files)
val base = if (all_known) deps(session).copy(known = deps.all_known) else deps(session)
- new Base_Info(sessions, deps, base)
+ new Base_Info(session, sessions, deps, base)
}
- final class Base_Info private [Sessions](val sessions: T, val deps: Deps, val base: Base)
+ final class Base_Info private [Sessions](
+ val session: String, val sessions: T, val deps: Deps, val base: Base)
{
- def platform_path: Base_Info = new Base_Info(sessions, deps, base.platform_path)
+ override def toString: String = session
def errors: List[String] = deps.errors
def check_base: Base = if (errors.isEmpty) base else error(cat_lines(errors))
--- a/src/Tools/jEdit/src/jedit_resources.scala Tue Oct 31 18:45:33 2017 +0100
+++ b/src/Tools/jEdit/src/jedit_resources.scala Tue Oct 31 18:56:24 2017 +0100
@@ -28,7 +28,7 @@
}
class JEdit_Resources private(session_base_info: Sessions.Base_Info)
- extends Resources(session_base_info.base)
+ extends Resources(session_base_info.base.platform_path)
{
def session_errors: List[String] = session_base_info.errors
--- a/src/Tools/jEdit/src/jedit_sessions.scala Tue Oct 31 18:45:33 2017 +0100
+++ b/src/Tools/jEdit/src/jedit_sessions.scala Tue Oct 31 18:56:24 2017 +0100
@@ -52,9 +52,7 @@
def session_base_info(options: Options): Sessions.Base_Info =
{
Sessions.session_base_info(options,
- session_name(options),
- dirs = JEdit_Sessions.session_dirs(),
- all_known = true).platform_path
+ session_name(options), dirs = JEdit_Sessions.session_dirs(), all_known = true)
}
def session_build_mode(): String = Isabelle_System.getenv("JEDIT_BUILD_MODE")