src/Pure/System/isabelle_process.ML
changeset 72112 3546dd4ade74
parent 72104 d9a42786fbc9
child 72114 d00220799735
equal deleted inserted replaced
72111:b9ded33bd58c 72112:3546dd4ade74
   111 fun recover crash =
   111 fun recover crash =
   112   (Synchronized.change crashes (cons crash);
   112   (Synchronized.change crashes (cons crash);
   113     Output.physical_stderr
   113     Output.physical_stderr
   114       "Recovered from Isabelle process crash -- see also Isabelle_Process.crashes\n");
   114       "Recovered from Isabelle process crash -- see also Isabelle_Process.crashes\n");
   115 
   115 
       
   116 val _ = Session.protocol_handler "isabelle.ML_Statistics$Protocol_Handler";
       
   117 
   116 in
   118 in
   117 
   119 
   118 fun init_protocol modes = Thread_Attributes.uninterruptible (fn _ => fn (address, password) =>
   120 fun init_protocol modes = Thread_Attributes.uninterruptible (fn _ => fn (address, password) =>
   119   let
   121   let
   120     val _ = SHA1.test_samples ()
   122     val _ = SHA1.test_samples ()
   197             else (Runtime.exn_system_message exn handle crash => recover crash);
   199             else (Runtime.exn_system_message exn handle crash => recover crash);
   198       in protocol_loop () end;
   200       in protocol_loop () end;
   199 
   201 
   200     fun protocol () =
   202     fun protocol () =
   201      (Session.init_protocol_handlers ();
   203      (Session.init_protocol_handlers ();
       
   204       Output.protocol_message (Markup.ml_pid (ML_PID.get ())) [];
   202       message Markup.initN [] [XML.Text (Session.welcome ())];
   205       message Markup.initN [] [XML.Text (Session.welcome ())];
   203       protocol_loop ());
   206       protocol_loop ());
   204 
   207 
   205     val result = Exn.capture (message_context protocol) ();
   208     val result = Exn.capture (message_context protocol) ();
   206 
   209 
   225 
   228 
   226 (* init options *)
   229 (* init options *)
   227 
   230 
   228 fun init_options () =
   231 fun init_options () =
   229  (ML_Print_Depth.set_print_depth (Options.default_int "ML_print_depth");
   232  (ML_Print_Depth.set_print_depth (Options.default_int "ML_print_depth");
   230   Future.ML_statistics := Options.default_bool "ML_statistics";
       
   231   Multithreading.trace := Options.default_int "threads_trace";
   233   Multithreading.trace := Options.default_int "threads_trace";
   232   Multithreading.max_threads_update (Options.default_int "threads");
   234   Multithreading.max_threads_update (Options.default_int "threads");
   233   Multithreading.parallel_proofs := Options.default_int "parallel_proofs";
   235   Multithreading.parallel_proofs := Options.default_int "parallel_proofs";
   234   if Options.default_bool "export_standard_proofs" then Proofterm.proofs := 2 else ();
   236   if Options.default_bool "export_standard_proofs" then Proofterm.proofs := 2 else ();
   235   let val proofs = Options.default_int "record_proofs"
   237   let val proofs = Options.default_int "record_proofs"