equal
deleted
inserted
replaced
78 val default_output_dir: Path = Path.explode("dump") |
78 val default_output_dir: Path = Path.explode("dump") |
79 |
79 |
80 def make_options(options: Options, aspects: List[Aspect]): Options = |
80 def make_options(options: Options, aspects: List[Aspect]): Options = |
81 { |
81 { |
82 val options0 = if (NUMA.enabled) NUMA.policy_options(options) else options |
82 val options0 = if (NUMA.enabled) NUMA.policy_options(options) else options |
83 val options1 = options0 + "completion_limit=0" + "ML_statistics=false" + "parallel_proofs=0" |
83 val options1 = |
|
84 options0 + "completion_limit=0" + "ML_statistics=false" + |
|
85 "parallel_proofs=0" + "editor_tracing_messages=0" |
84 (options1 /: aspects)({ case (opts, aspect) => (opts /: aspect.options)(_ + _) }) |
86 (options1 /: aspects)({ case (opts, aspect) => (opts /: aspect.options)(_ + _) }) |
85 } |
87 } |
86 |
88 |
87 def dump(options: Options, logic: String, |
89 def dump(options: Options, logic: String, |
88 aspects: List[Aspect] = Nil, |
90 aspects: List[Aspect] = Nil, |