tuned;
authorwenzelm
Mon Sep 03 18:45:03 2018 +0200 (9 months ago)
changeset 68895cca4555f412d
parent 68894 1dbdad1b57a5
child 68896 e63eaae13165
tuned;
src/Pure/Tools/dump.scala
     1.1 --- a/src/Pure/Tools/dump.scala	Mon Sep 03 16:23:26 2018 +0200
     1.2 +++ b/src/Pure/Tools/dump.scala	Mon Sep 03 18:45:03 2018 +0200
     1.3 @@ -79,8 +79,10 @@
     1.4    val default_output_dir = Path.explode("dump")
     1.5  
     1.6    def make_options(options: Options, aspects: List[Aspect]): Options =
     1.7 -    (options.int.update("completion_limit", 0).bool.update("ML_statistics", false) /: aspects)(
     1.8 -      { case (opts, aspect) => (opts /: aspect.options)(_ + _) })
     1.9 +  {
    1.10 +    val options1 = options + "completion_limit=0" + "ML_statistics=false"
    1.11 +    (options1 /: aspects)({ case (opts, aspect) => (opts /: aspect.options)(_ + _) })
    1.12 +  }
    1.13  
    1.14    def dump(options: Options, logic: String,
    1.15      aspects: List[Aspect] = Nil,