src/Pure/Tools/dump.scala
changeset 70857 822f5cbfc5b6
parent 70856 545229df2f82
child 70858 f76126e6a1ab
equal deleted inserted replaced
70856:545229df2f82 70857:822f5cbfc5b6
   123     val session_options: Options,
   123     val session_options: Options,
   124     val deps: Sessions.Deps)
   124     val deps: Sessions.Deps)
   125   {
   125   {
   126     def session_dirs: List[Path] = dirs ::: select_dirs
   126     def session_dirs: List[Path] = dirs ::: select_dirs
   127 
   127 
       
   128     def build_logic(logic: String)
       
   129     {
       
   130       Build.build_logic(options, logic, build_heap = true, progress = progress,
       
   131         dirs = session_dirs, strict = true)
       
   132     }
       
   133 
   128     def session(logic: String, log: Logger = No_Logger): Session =
   134     def session(logic: String, log: Logger = No_Logger): Session =
       
   135     {
       
   136       build_logic(logic)
   129       new Session(this, logic, log)
   137       new Session(this, logic, log)
       
   138     }
   130   }
   139   }
   131 
   140 
   132   class Session private[Dump](context: Context, logic: String, log: Logger)
   141   class Session private[Dump](context: Context, logic: String, log: Logger)
   133   {
   142   {
   134     /* resources */
   143     /* resources */
   135 
   144 
   136     private val progress = context.progress
   145     private val progress = context.progress
   137 
       
   138     Build.build_logic(context.options, logic, build_heap = true, progress = progress,
       
   139       dirs = context.session_dirs, strict = true)
       
   140 
   146 
   141     val resources: Headless.Resources =
   147     val resources: Headless.Resources =
   142       Headless.Resources.make(context.session_options, logic, progress = progress, log = log,
   148       Headless.Resources.make(context.session_options, logic, progress = progress, log = log,
   143         session_dirs = context.session_dirs,
   149         session_dirs = context.session_dirs,
   144         include_sessions = context.deps.sessions_structure.imports_topological_order)
   150         include_sessions = context.deps.sessions_structure.imports_topological_order)