--- a/src/Pure/Tools/dump.scala Mon Oct 14 12:07:37 2019 +0200
+++ b/src/Pure/Tools/dump.scala Mon Oct 14 13:17:33 2019 +0200
@@ -125,8 +125,17 @@
{
def session_dirs: List[Path] = dirs ::: select_dirs
+ def build_logic(logic: String)
+ {
+ Build.build_logic(options, logic, build_heap = true, progress = progress,
+ dirs = session_dirs, strict = true)
+ }
+
def session(logic: String, log: Logger = No_Logger): Session =
+ {
+ build_logic(logic)
new Session(this, logic, log)
+ }
}
class Session private[Dump](context: Context, logic: String, log: Logger)
@@ -135,9 +144,6 @@
private val progress = context.progress
- Build.build_logic(context.options, logic, build_heap = true, progress = progress,
- dirs = context.session_dirs, strict = true)
-
val resources: Headless.Resources =
Headless.Resources.make(context.session_options, logic, progress = progress, log = log,
session_dirs = context.session_dirs,