clarified signature;
authorwenzelm
Tue Oct 31 18:56:24 2017 +0100 (18 months ago)
changeset 669659cec50354099
parent 66964 9f2de457b95e
child 66966 f3f9a492bee6
clarified signature;
src/Pure/Thy/sessions.scala
src/Tools/jEdit/src/jedit_resources.scala
src/Tools/jEdit/src/jedit_sessions.scala
     1.1 --- a/src/Pure/Thy/sessions.scala	Tue Oct 31 18:45:33 2017 +0100
     1.2 +++ b/src/Pure/Thy/sessions.scala	Tue Oct 31 18:56:24 2017 +0100
     1.3 @@ -336,12 +336,13 @@
     1.4      val deps = Sessions.deps(sessions, global_theories, inlined_files = inlined_files)
     1.5      val base = if (all_known) deps(session).copy(known = deps.all_known) else deps(session)
     1.6  
     1.7 -    new Base_Info(sessions, deps, base)
     1.8 +    new Base_Info(session, sessions, deps, base)
     1.9    }
    1.10  
    1.11 -  final class Base_Info private [Sessions](val sessions: T, val deps: Deps, val base: Base)
    1.12 +  final class Base_Info private [Sessions](
    1.13 +    val session: String, val sessions: T, val deps: Deps, val base: Base)
    1.14    {
    1.15 -    def platform_path: Base_Info = new Base_Info(sessions, deps, base.platform_path)
    1.16 +    override def toString: String = session
    1.17  
    1.18      def errors: List[String] = deps.errors
    1.19      def check_base: Base = if (errors.isEmpty) base else error(cat_lines(errors))
     2.1 --- a/src/Tools/jEdit/src/jedit_resources.scala	Tue Oct 31 18:45:33 2017 +0100
     2.2 +++ b/src/Tools/jEdit/src/jedit_resources.scala	Tue Oct 31 18:56:24 2017 +0100
     2.3 @@ -28,7 +28,7 @@
     2.4  }
     2.5  
     2.6  class JEdit_Resources private(session_base_info: Sessions.Base_Info)
     2.7 -  extends Resources(session_base_info.base)
     2.8 +  extends Resources(session_base_info.base.platform_path)
     2.9  {
    2.10    def session_errors: List[String] = session_base_info.errors
    2.11  
     3.1 --- a/src/Tools/jEdit/src/jedit_sessions.scala	Tue Oct 31 18:45:33 2017 +0100
     3.2 +++ b/src/Tools/jEdit/src/jedit_sessions.scala	Tue Oct 31 18:56:24 2017 +0100
     3.3 @@ -52,9 +52,7 @@
     3.4    def session_base_info(options: Options): Sessions.Base_Info =
     3.5    {
     3.6      Sessions.session_base_info(options,
     3.7 -      session_name(options),
     3.8 -      dirs = JEdit_Sessions.session_dirs(),
     3.9 -      all_known = true).platform_path
    3.10 +      session_name(options), dirs = JEdit_Sessions.session_dirs(), all_known = true)
    3.11    }
    3.12  
    3.13    def session_build_mode(): String = Isabelle_System.getenv("JEDIT_BUILD_MODE")