src/Pure/Tools/dump.scala
changeset 70659 44588e355ca8
parent 70655 f51955effb02
child 70670 a1dfd603260e
equal deleted inserted replaced
70658:4655897b8287 70659:44588e355ca8
   129     }
   129     }
   130 
   130 
   131     val deps: Sessions.Deps =
   131     val deps: Sessions.Deps =
   132       Sessions.load_structure(dump_options, dirs = dirs, select_dirs = select_dirs).
   132       Sessions.load_structure(dump_options, dirs = dirs, select_dirs = select_dirs).
   133         selection_deps(dump_options, selection, progress = progress,
   133         selection_deps(dump_options, selection, progress = progress,
   134           uniform_session = true, loading_sessions = true)
   134           uniform_session = true, loading_sessions = true).check_errors
   135 
   135 
   136     val resources: Headless.Resources =
   136     val resources: Headless.Resources =
   137       Headless.Resources.make(dump_options, logic, progress = progress, log = log,
   137       Headless.Resources.make(dump_options, logic, progress = progress, log = log,
   138         session_dirs = dirs ::: select_dirs,
   138         session_dirs = dirs ::: select_dirs,
   139         include_sessions = deps.sessions_structure.imports_topological_order)
   139         include_sessions = deps.sessions_structure.imports_topological_order)