src/Pure/Tools/dump.scala
changeset 68416 33114721ac9a
parent 68365 f9379279f98c
child 68491 f0f83ce0badd
     1.1 --- a/src/Pure/Tools/dump.scala	Mon Jun 11 08:15:43 2018 +0200
     1.2 +++ b/src/Pure/Tools/dump.scala	Mon Jun 11 15:50:28 2018 +0200
     1.3 @@ -78,6 +78,10 @@
     1.4  
     1.5    val default_output_dir = Path.explode("dump")
     1.6  
     1.7 +  def make_options(options: Options, aspects: List[Aspect]): Options =
     1.8 +    (options.int.update("completion_limit", 0).bool.update("ML_statistics", false) /: aspects)(
     1.9 +      { case (opts, aspect) => (opts /: aspect.options)(_ + _) })
    1.10 +
    1.11    def dump(options: Options, logic: String,
    1.12      aspects: List[Aspect] = Nil,
    1.13      progress: Progress = No_Progress,
    1.14 @@ -92,9 +96,7 @@
    1.15      if (Build.build_logic(options, logic, progress = progress, dirs = dirs,
    1.16        system_mode = system_mode) != 0) error(logic + " FAILED")
    1.17  
    1.18 -    val dump_options =
    1.19 -      (options.int.update("completion_limit", 0).bool.update("ML_statistics", false) /: aspects)(
    1.20 -        { case (opts, aspect) => (opts /: aspect.options)(_ + _) })
    1.21 +    val dump_options = make_options(options, aspects)
    1.22  
    1.23  
    1.24      /* dependencies */