# HG changeset patch # User wenzelm # Date 1571051853 -7200 # Node ID 822f5cbfc5b6782b7be2b956d660413cb0381c6d # Parent 545229df2f823acf4b4ff21593fc28cf25272a60 tuned signature; diff -r 545229df2f82 -r 822f5cbfc5b6 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,