equal
deleted
inserted
replaced
104 val session_options: Options = |
104 val session_options: Options = |
105 { |
105 { |
106 val options0 = if (NUMA.enabled) NUMA.policy_options(options) else options |
106 val options0 = if (NUMA.enabled) NUMA.policy_options(options) else options |
107 val options1 = |
107 val options1 = |
108 options0 + |
108 options0 + |
109 "ML_statistics=false" + |
|
110 "parallel_proofs=0" + |
109 "parallel_proofs=0" + |
111 "completion_limit=0" + |
110 "completion_limit=0" + |
112 "editor_tracing_messages=0" + |
111 "editor_tracing_messages=0" + |
113 "editor_presentation" |
112 "editor_presentation" |
114 (options1 /: aspects)({ case (opts, aspect) => (opts /: aspect.options)(_ + _) }) |
113 (options1 /: aspects)({ case (opts, aspect) => (opts /: aspect.options)(_ + _) }) |