# HG changeset patch
# User wenzelm
# Date 1509472584 -3600
# Node ID 9cec5035409944bdc404efec242bbb65fe25217a
# Parent  9f2de457b95e2c9e9e6f03ec42ad71b0cd177f46
clarified signature;

diff -r 9f2de457b95e -r 9cec50354099 src/Pure/Thy/sessions.scala
--- 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))
diff -r 9f2de457b95e -r 9cec50354099 src/Tools/jEdit/src/jedit_resources.scala
--- 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
 
diff -r 9f2de457b95e -r 9cec50354099 src/Tools/jEdit/src/jedit_sessions.scala
--- 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")