clarified signature;
authorwenzelm
Sat, 24 Mar 2018 22:45:06 +0100
changeset 67948 83902fff6243
parent 67947 ad735a551a11
child 67949 4bb49ed64933
child 67950 99eaa5cedbb7
clarified signature;
src/Pure/Thy/thy_resources.scala
--- a/src/Pure/Thy/thy_resources.scala	Sat Mar 24 22:10:14 2018 +0100
+++ b/src/Pure/Thy/thy_resources.scala	Sat Mar 24 22:45:06 2018 +0100
@@ -18,6 +18,7 @@
     options: Options,
     session_name: String,
     session_dirs: List[Path] = Nil,
+    include_sessions: List[String] = Nil,
     session_base: Option[Sessions.Base] = None,
     print_mode: List[String] = Nil,
     progress: Progress = No_Progress,
@@ -25,7 +26,8 @@
   {
     val base =
       session_base getOrElse
-      Sessions.base_info(options, session_name, progress = progress, dirs = session_dirs).check_base
+        Sessions.base_info(options, session_name, include_sessions = include_sessions,
+          progress = progress, dirs = session_dirs).check_base
     val resources = new Thy_Resources(base, log = log)
     val session = new Session(session_name, options, resources)