# HG changeset patch # User wenzelm # Date 1585656576 -7200 # Node ID 45c2b8cf1b26f086b87da99b66e1501e6f523b96 # Parent c1bc38327bc21f7f925bbe260c645db860b0ec0a more robust message_context and shutdown, e.g. after errors in protocol loop (see also 3f02bc5a5a03); diff -r c1bc38327bc2 -r 45c2b8cf1b26 src/Pure/General/output.ML --- a/src/Pure/General/output.ML Mon Mar 30 19:50:01 2020 +0200 +++ b/src/Pure/General/output.ML Tue Mar 31 14:09:36 2020 +0200 @@ -59,7 +59,6 @@ val report_fn: (output list -> unit) Unsynchronized.ref val result_fn: (Properties.T -> output list -> unit) Unsynchronized.ref val protocol_message_fn: Output_Primitives.protocol_message_fn Unsynchronized.ref - val init_channels: unit -> unit end; structure Private_Output: PRIVATE_OUTPUT = diff -r c1bc38327bc2 -r 45c2b8cf1b26 src/Pure/System/isabelle_process.ML --- a/src/Pure/System/isabelle_process.ML Mon Mar 30 19:50:01 2020 +0200 +++ b/src/Pure/System/isabelle_process.ML Tue Mar 31 14:09:36 2020 +0200 @@ -28,6 +28,9 @@ val _ = Output.add_mode isabelle_processN Output.default_output Output.default_escape; val _ = Markup.add_mode isabelle_processN YXML.output_markup; +val protocol_modes1 = [Syntax_Trans.no_bracketsN, Syntax_Trans.no_type_bracketsN]; +val protocol_modes2 = [isabelle_processN, Pretty.symbolicN]; + (* protocol commands *) @@ -92,16 +95,43 @@ end); -(* output channels *) +(* init protocol -- uninterruptible *) + +exception EXIT of exn; + +val crashes = Synchronized.var "Isabelle_Process.crashes" ([]: exn list); + +local + +fun recover crash = + (Synchronized.change crashes (cons crash); + Output.physical_stderr + "Recovered from Isabelle process crash -- see also Isabelle_Process.crashes\n"); + +in -val serial_props = Markup.serial_properties o serial; +val init_protocol = Thread_Attributes.uninterruptible (fn _ => fn (address, password) => + let + val _ = SHA1.test_samples () + handle exn as Fail msg => (Output.physical_stderr (msg ^ "\n"); Exn.reraise exn); + + val _ = Output.physical_stderr Symbol.STX; -fun init_channels out_stream = - let + val _ = Context.put_generic_context NONE; + + + (* streams *) + + val (in_stream, out_stream) = Socket_IO.open_streams address; + val _ = Byte_Message.write_line out_stream password; + val _ = TextIO.StreamIO.setBufferMode (TextIO.getOutstream TextIO.stdOut, IO.LINE_BUF); val _ = TextIO.StreamIO.setBufferMode (TextIO.getOutstream TextIO.stdErr, IO.LINE_BUF); val _ = BinIO.StreamIO.setBufferMode (BinIO.getOutstream out_stream, IO.BLOCK_BUF); + + (* messages *) + val msg_channel = Message_Channel.make out_stream; fun message name props body = @@ -116,90 +146,70 @@ (false, SOME id') => props @ [(Markup.idN, id')] | _ => props); in message name props' (XML.blob ss) end; - in - Private_Output.status_fn := standard_message [] Markup.statusN; - Private_Output.report_fn := standard_message [] Markup.reportN; - Private_Output.result_fn := - (fn props => fn s => standard_message (props @ serial_props ()) Markup.resultN s); - Private_Output.writeln_fn := (fn s => standard_message (serial_props ()) Markup.writelnN s); - Private_Output.state_fn := (fn s => standard_message (serial_props ()) Markup.stateN s); - Private_Output.information_fn := - (fn s => standard_message (serial_props ()) Markup.informationN s); - Private_Output.tracing_fn := - (fn s => (update_tracing (); standard_message (serial_props ()) Markup.tracingN s)); - Private_Output.warning_fn := (fn s => standard_message (serial_props ()) Markup.warningN s); - Private_Output.legacy_fn := (fn s => standard_message (serial_props ()) Markup.legacyN s); - Private_Output.error_message_fn := - (fn (i, s) => standard_message (Markup.serial_properties i) Markup.errorN s); - Private_Output.system_message_fn := - (fn ss => message Markup.systemN [] (XML.blob ss)); - Private_Output.protocol_message_fn := - (fn props => fn body => message Markup.protocolN props body); + + val serial_props = Markup.serial_properties o serial; - Session.init_protocol_handlers (); - message Markup.initN [] [XML.Text (Session.welcome ())]; - msg_channel - end; + val message_context = + Unsynchronized.setmp Private_Output.status_fn + (standard_message [] Markup.statusN) #> + Unsynchronized.setmp Private_Output.report_fn + (standard_message [] Markup.reportN) #> + Unsynchronized.setmp Private_Output.result_fn + (fn props => fn s => standard_message (props @ serial_props ()) Markup.resultN s) #> + Unsynchronized.setmp Private_Output.writeln_fn + (fn s => standard_message (serial_props ()) Markup.writelnN s) #> + Unsynchronized.setmp Private_Output.state_fn + (fn s => standard_message (serial_props ()) Markup.stateN s) #> + Unsynchronized.setmp Private_Output.information_fn + (fn s => standard_message (serial_props ()) Markup.informationN s) #> + Unsynchronized.setmp Private_Output.tracing_fn + (fn s => (update_tracing (); standard_message (serial_props ()) Markup.tracingN s)) #> + Unsynchronized.setmp Private_Output.warning_fn + (fn s => standard_message (serial_props ()) Markup.warningN s) #> + Unsynchronized.setmp Private_Output.legacy_fn + (fn s => standard_message (serial_props ()) Markup.legacyN s) #> + Unsynchronized.setmp Private_Output.error_message_fn + (fn (i, s) => standard_message (Markup.serial_properties i) Markup.errorN s) #> + Unsynchronized.setmp Private_Output.system_message_fn + (fn ss => message Markup.systemN [] (XML.blob ss)) #> + Unsynchronized.setmp Private_Output.protocol_message_fn + (fn props => fn body => message Markup.protocolN props body) #> + Unsynchronized.setmp print_mode + ((! print_mode @ protocol_modes1) |> fold (update op =) protocol_modes2); -(* protocol loop -- uninterruptible *) - -exception EXIT of exn; - -val crashes = Synchronized.var "Isabelle_Process.crashes" ([]: exn list); + (* protocol *) -local - -fun recover crash = - (Synchronized.change crashes (cons crash); - Output.physical_stderr - "Recovered from Isabelle process crash -- see also Isabelle_Process.crashes\n"); + fun protocol_loop () = + let + val continue = + (case Byte_Message.read_message in_stream of + NONE => false + | SOME [] => (Output.system_message "Isabelle process: no input"; true) + | SOME (name :: args) => (run_command name args; true)) + handle EXIT exn => Exn.reraise exn + | exn => (Runtime.exn_system_message exn handle crash => recover crash; true); + in if continue then protocol_loop () else () end; -fun shutdown () = (Future.shutdown (); ignore (Execution.reset ())); + fun protocol () = + (Session.init_protocol_handlers (); + message Markup.initN [] [XML.Text (Session.welcome ())]; + protocol_loop ()); -in + val result = Exn.capture (message_context protocol) (); + -fun loop stream = - let - val continue = - (case Byte_Message.read_message stream of - NONE => false - | SOME [] => (Output.system_message "Isabelle process: no input"; true) - | SOME (name :: args) => (run_command name args; true)) - handle EXIT exn => (shutdown (); Exn.reraise exn) - | exn => (Runtime.exn_system_message exn handle crash => recover crash; true); - in if continue then loop stream else shutdown () end; + (* shutdown *) + + val _ = Future.shutdown (); + val _ = Execution.reset (); + val _ = Message_Channel.shutdown msg_channel; + + in Exn.release result end); end; -(* init protocol *) - -val default_modes1 = [Syntax_Trans.no_bracketsN, Syntax_Trans.no_type_bracketsN]; -val default_modes2 = [isabelle_processN, Pretty.symbolicN]; - -val init_protocol = Thread_Attributes.uninterruptible (fn _ => fn (address, password) => - let - val _ = SHA1.test_samples () - handle exn as Fail msg => (Output.physical_stderr (msg ^ "\n"); Exn.reraise exn); - val _ = Output.physical_stderr Symbol.STX; - - val _ = Context.put_generic_context NONE; - val _ = - Unsynchronized.change print_mode - (fn mode => (mode @ default_modes1) |> fold (update op =) default_modes2); - - val (in_stream, out_stream) = Socket_IO.open_streams address; - val _ = Byte_Message.write_line out_stream password; - val msg_channel = init_channels out_stream; - val _ = loop in_stream; - val _ = Message_Channel.shutdown msg_channel; - val _ = Private_Output.init_channels (); - - val _ = print_mode := []; - in () end); - - (* init options *) fun init_options () =