tuned signature;
authorwenzelm
Mon, 14 Oct 2019 13:17:33 +0200
changeset 70857 822f5cbfc5b6
parent 70856 545229df2f82
child 70858 f76126e6a1ab
tuned signature;
src/Pure/Tools/dump.scala
--- 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,