--- a/src/Pure/Thy/thy_resources.scala Sun Nov 12 20:12:10 2017 +0100
+++ b/src/Pure/Thy/thy_resources.scala Sun Nov 12 20:17:29 2017 +0100
@@ -15,11 +15,14 @@
options: Options,
session_name: String,
session_dirs: List[Path] = Nil,
+ session_base: Option[Sessions.Base] = None,
modes: List[String] = Nil,
log: Logger = No_Logger): Session =
{
- val session_base = Sessions.base_info(options, session_name, dirs = session_dirs).check_base
- val resources = new Thy_Resources(session_base, log = log)
+ val base =
+ session_base getOrElse
+ Sessions.base_info(options, session_name, dirs = session_dirs).check_base
+ val resources = new Thy_Resources(base, log = log)
val session = new Session(options, resources)
val session_error = Future.promise[String]