src/Pure/Tools/dump.scala
changeset 69522 9457d85204f5
parent 69521 0428fd0a13b7
child 69523 9403ff523825
equal deleted inserted replaced
69521:0428fd0a13b7 69522:9457d85204f5
    91     progress: Progress = No_Progress,
    91     progress: Progress = No_Progress,
    92     log: Logger = No_Logger,
    92     log: Logger = No_Logger,
    93     dirs: List[Path] = Nil,
    93     dirs: List[Path] = Nil,
    94     select_dirs: List[Path] = Nil,
    94     select_dirs: List[Path] = Nil,
    95     output_dir: Path = default_output_dir,
    95     output_dir: Path = default_output_dir,
    96     verbose: Boolean = false,
       
    97     system_mode: Boolean = false,
    96     system_mode: Boolean = false,
    98     selection: Sessions.Selection = Sessions.Selection.empty): Boolean =
    97     selection: Sessions.Selection = Sessions.Selection.empty): Boolean =
    99   {
    98   {
   100     if (Build.build_logic(options, logic, build_heap = true, progress = progress,
    99     if (Build.build_logic(options, logic, build_heap = true, progress = progress,
   101       dirs = dirs ::: select_dirs, system_mode = system_mode) != 0) error(logic + " FAILED")
   100       dirs = dirs ::: select_dirs, system_mode = system_mode) != 0) error(logic + " FAILED")
   243             aspects = aspects,
   242             aspects = aspects,
   244             progress = progress,
   243             progress = progress,
   245             dirs = dirs,
   244             dirs = dirs,
   246             select_dirs = select_dirs,
   245             select_dirs = select_dirs,
   247             output_dir = output_dir,
   246             output_dir = output_dir,
   248             verbose = verbose,
       
   249             selection = Sessions.Selection(
   247             selection = Sessions.Selection(
   250               requirements = requirements,
   248               requirements = requirements,
   251               all_sessions = all_sessions,
   249               all_sessions = all_sessions,
   252               base_sessions = base_sessions,
   250               base_sessions = base_sessions,
   253               exclude_session_groups = exclude_session_groups,
   251               exclude_session_groups = exclude_session_groups,