clarified signature;
authorwenzelm
Sat Mar 24 22:45:06 2018 +0100 (14 months ago)
changeset 6794883902fff6243
parent 67947 ad735a551a11
child 67949 4bb49ed64933
child 67950 99eaa5cedbb7
clarified signature;
src/Pure/Thy/thy_resources.scala
     1.1 --- a/src/Pure/Thy/thy_resources.scala	Sat Mar 24 22:10:14 2018 +0100
     1.2 +++ b/src/Pure/Thy/thy_resources.scala	Sat Mar 24 22:45:06 2018 +0100
     1.3 @@ -18,6 +18,7 @@
     1.4      options: Options,
     1.5      session_name: String,
     1.6      session_dirs: List[Path] = Nil,
     1.7 +    include_sessions: List[String] = Nil,
     1.8      session_base: Option[Sessions.Base] = None,
     1.9      print_mode: List[String] = Nil,
    1.10      progress: Progress = No_Progress,
    1.11 @@ -25,7 +26,8 @@
    1.12    {
    1.13      val base =
    1.14        session_base getOrElse
    1.15 -      Sessions.base_info(options, session_name, progress = progress, dirs = session_dirs).check_base
    1.16 +        Sessions.base_info(options, session_name, include_sessions = include_sessions,
    1.17 +          progress = progress, dirs = session_dirs).check_base
    1.18      val resources = new Thy_Resources(base, log = log)
    1.19      val session = new Session(session_name, options, resources)
    1.20