equal
deleted
inserted
replaced
63 end; |
63 end; |
64 |
64 |
65 |
65 |
66 (* tracing limit *) |
66 (* tracing limit *) |
67 |
67 |
68 val tracing_limit = Unsynchronized.ref 500000; |
68 val tracing_limit = Unsynchronized.ref 1000000; |
69 |
69 |
70 val tracing_limits = Synchronized.var "tracing_limits" (Inttab.empty: int Inttab.table); |
70 val tracing_limits = Synchronized.var "tracing_limits" (Inttab.empty: int Inttab.table); |
71 |
71 |
72 fun reset_tracing_limits () = Synchronized.change tracing_limits (K Inttab.empty); |
72 fun reset_tracing_limits () = Synchronized.change tracing_limits (K Inttab.empty); |
73 |
73 |
222 Multithreading.trace := Options.int options "threads_trace"; |
222 Multithreading.trace := Options.int options "threads_trace"; |
223 Multithreading.max_threads := Options.int options "threads"; |
223 Multithreading.max_threads := Options.int options "threads"; |
224 if Multithreading.max_threads_value () < 2 |
224 if Multithreading.max_threads_value () < 2 |
225 then Multithreading.max_threads := 2 else (); |
225 then Multithreading.max_threads := 2 else (); |
226 Goal.parallel_proofs := (if Options.int options "parallel_proofs" > 0 then 4 else 0); |
226 Goal.parallel_proofs := (if Options.int options "parallel_proofs" > 0 then 4 else 0); |
227 Goal.parallel_proofs_threshold := Options.int options "parallel_proofs_threshold" |
227 Goal.parallel_proofs_threshold := Options.int options "parallel_proofs_threshold"; |
|
228 tracing_limit := Options.int options "editor_tracing_limit" |
228 end); |
229 end); |
229 |
230 |
230 end; |
231 end; |
231 |
232 |