src/Pure/System/isabelle_process.ML
changeset 78711 3a3a70d4d422
parent 78018 dfa44d85d751
child 78725 3c02ad5a1586
equal deleted inserted replaced
78710:27b2368ca69d 78711:3a3a70d4d422
   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";