equal
deleted
inserted
replaced
195 fun init_options () = |
195 fun init_options () = |
196 (ML_Print_Depth.set_print_depth (Options.default_int "ML_print_depth"); |
196 (ML_Print_Depth.set_print_depth (Options.default_int "ML_print_depth"); |
197 Multithreading.trace := Options.default_int "threads_trace"; |
197 Multithreading.trace := Options.default_int "threads_trace"; |
198 Multithreading.max_threads_update (Options.default_int "threads"); |
198 Multithreading.max_threads_update (Options.default_int "threads"); |
199 Multithreading.parallel_proofs := Options.default_int "parallel_proofs"; |
199 Multithreading.parallel_proofs := Options.default_int "parallel_proofs"; |
|
200 Isabelle_Thread.threads_stack_limit := Options.default_real "threads_stack_limit"; |
200 if Options.default_bool "export_standard_proofs" then Proofterm.proofs := 2 else (); |
201 if Options.default_bool "export_standard_proofs" then Proofterm.proofs := 2 else (); |
201 let val proofs = Options.default_int "record_proofs" |
202 let val proofs = Options.default_int "record_proofs" |
202 in if proofs < 0 then () else Proofterm.proofs := proofs end; |
203 in if proofs < 0 then () else Proofterm.proofs := proofs end; |
203 Printer.show_markup_default := false; |
204 Printer.show_markup_default := false; |
204 Context.theory_tracing := Options.default_bool "context_theory_tracing"; |
205 Context.theory_tracing := Options.default_bool "context_theory_tracing"; |