src/Pure/System/isabelle_process.ML
changeset 71852 45c2b8cf1b26
parent 71847 3f02bc5a5a03
child 71853 ec14ef6dd09b
equal deleted inserted replaced
71848:c1bc38327bc2 71852:45c2b8cf1b26
    25 
    25 
    26 fun is_active () = Print_Mode.print_mode_active isabelle_processN;
    26 fun is_active () = Print_Mode.print_mode_active isabelle_processN;
    27 
    27 
    28 val _ = Output.add_mode isabelle_processN Output.default_output Output.default_escape;
    28 val _ = Output.add_mode isabelle_processN Output.default_output Output.default_escape;
    29 val _ = Markup.add_mode isabelle_processN YXML.output_markup;
    29 val _ = Markup.add_mode isabelle_processN YXML.output_markup;
       
    30 
       
    31 val protocol_modes1 = [Syntax_Trans.no_bracketsN, Syntax_Trans.no_type_bracketsN];
       
    32 val protocol_modes2 = [isabelle_processN, Pretty.symbolicN];
    30 
    33 
    31 
    34 
    32 (* protocol commands *)
    35 (* protocol commands *)
    33 
    36 
    34 local
    37 local
    90               (Inttab.map_default (exec_id, 0) (fn k => k - m))
    93               (Inttab.map_default (exec_id, 0) (fn k => k - m))
    91           end
    94           end
    92       end);
    95       end);
    93 
    96 
    94 
    97 
    95 (* output channels *)
    98 (* init protocol -- uninterruptible *)
    96 
    99 
    97 val serial_props = Markup.serial_properties o serial;
   100 exception EXIT of exn;
    98 
   101 
    99 fun init_channels out_stream =
   102 val crashes = Synchronized.var "Isabelle_Process.crashes" ([]: exn list);
       
   103 
       
   104 local
       
   105 
       
   106 fun recover crash =
       
   107   (Synchronized.change crashes (cons crash);
       
   108     Output.physical_stderr
       
   109       "Recovered from Isabelle process crash -- see also Isabelle_Process.crashes\n");
       
   110 
       
   111 in
       
   112 
       
   113 val init_protocol = Thread_Attributes.uninterruptible (fn _ => fn (address, password) =>
   100   let
   114   let
       
   115     val _ = SHA1.test_samples ()
       
   116       handle exn as Fail msg => (Output.physical_stderr (msg ^ "\n"); Exn.reraise exn);
       
   117 
       
   118     val _ = Output.physical_stderr Symbol.STX;
       
   119 
       
   120     val _ = Context.put_generic_context NONE;
       
   121 
       
   122 
       
   123     (* streams *)
       
   124 
       
   125     val (in_stream, out_stream) = Socket_IO.open_streams address;
       
   126     val _ = Byte_Message.write_line out_stream password;
       
   127 
   101     val _ = TextIO.StreamIO.setBufferMode (TextIO.getOutstream TextIO.stdOut, IO.LINE_BUF);
   128     val _ = TextIO.StreamIO.setBufferMode (TextIO.getOutstream TextIO.stdOut, IO.LINE_BUF);
   102     val _ = TextIO.StreamIO.setBufferMode (TextIO.getOutstream TextIO.stdErr, IO.LINE_BUF);
   129     val _ = TextIO.StreamIO.setBufferMode (TextIO.getOutstream TextIO.stdErr, IO.LINE_BUF);
   103     val _ = BinIO.StreamIO.setBufferMode (BinIO.getOutstream out_stream, IO.BLOCK_BUF);
   130     val _ = BinIO.StreamIO.setBufferMode (BinIO.getOutstream out_stream, IO.BLOCK_BUF);
       
   131 
       
   132 
       
   133     (* messages *)
   104 
   134 
   105     val msg_channel = Message_Channel.make out_stream;
   135     val msg_channel = Message_Channel.make out_stream;
   106 
   136 
   107     fun message name props body =
   137     fun message name props body =
   108       Message_Channel.send msg_channel (Message_Channel.message name props body);
   138       Message_Channel.send msg_channel (Message_Channel.message name props body);
   114           val props' =
   144           val props' =
   115             (case (Properties.defined props Markup.idN, Position.get_id (Position.thread_data ())) of
   145             (case (Properties.defined props Markup.idN, Position.get_id (Position.thread_data ())) of
   116               (false, SOME id') => props @ [(Markup.idN, id')]
   146               (false, SOME id') => props @ [(Markup.idN, id')]
   117             | _ => props);
   147             | _ => props);
   118         in message name props' (XML.blob ss) end;
   148         in message name props' (XML.blob ss) end;
   119   in
   149 
   120     Private_Output.status_fn := standard_message [] Markup.statusN;
   150     val serial_props = Markup.serial_properties o serial;
   121     Private_Output.report_fn := standard_message [] Markup.reportN;
   151 
   122     Private_Output.result_fn :=
   152     val message_context =
   123       (fn props => fn s => standard_message (props @ serial_props ()) Markup.resultN s);
   153       Unsynchronized.setmp Private_Output.status_fn
   124     Private_Output.writeln_fn := (fn s => standard_message (serial_props ()) Markup.writelnN s);
   154         (standard_message [] Markup.statusN) #>
   125     Private_Output.state_fn := (fn s => standard_message (serial_props ()) Markup.stateN s);
   155       Unsynchronized.setmp Private_Output.report_fn
   126     Private_Output.information_fn :=
   156         (standard_message [] Markup.reportN) #>
   127       (fn s => standard_message (serial_props ()) Markup.informationN s);
   157       Unsynchronized.setmp Private_Output.result_fn
   128     Private_Output.tracing_fn :=
   158         (fn props => fn s => standard_message (props @ serial_props ()) Markup.resultN s) #>
   129       (fn s => (update_tracing (); standard_message (serial_props ()) Markup.tracingN s));
   159       Unsynchronized.setmp Private_Output.writeln_fn
   130     Private_Output.warning_fn := (fn s => standard_message (serial_props ()) Markup.warningN s);
   160         (fn s => standard_message (serial_props ()) Markup.writelnN s) #>
   131     Private_Output.legacy_fn := (fn s => standard_message (serial_props ()) Markup.legacyN s);
   161       Unsynchronized.setmp Private_Output.state_fn
   132     Private_Output.error_message_fn :=
   162         (fn s => standard_message (serial_props ()) Markup.stateN s) #>
   133       (fn (i, s) => standard_message (Markup.serial_properties i) Markup.errorN s);
   163       Unsynchronized.setmp Private_Output.information_fn
   134     Private_Output.system_message_fn :=
   164         (fn s => standard_message (serial_props ()) Markup.informationN s) #>
   135       (fn ss => message Markup.systemN [] (XML.blob ss));
   165       Unsynchronized.setmp Private_Output.tracing_fn
   136     Private_Output.protocol_message_fn :=
   166         (fn s => (update_tracing (); standard_message (serial_props ()) Markup.tracingN s)) #>
   137       (fn props => fn body => message Markup.protocolN props body);
   167       Unsynchronized.setmp Private_Output.warning_fn
   138 
   168         (fn s => standard_message (serial_props ()) Markup.warningN s) #>
   139     Session.init_protocol_handlers ();
   169       Unsynchronized.setmp Private_Output.legacy_fn
   140     message Markup.initN [] [XML.Text (Session.welcome ())];
   170         (fn s => standard_message (serial_props ()) Markup.legacyN s) #>
   141     msg_channel
   171       Unsynchronized.setmp Private_Output.error_message_fn
   142   end;
   172         (fn (i, s) => standard_message (Markup.serial_properties i) Markup.errorN s) #>
   143 
   173       Unsynchronized.setmp Private_Output.system_message_fn
   144 
   174         (fn ss => message Markup.systemN [] (XML.blob ss)) #>
   145 (* protocol loop -- uninterruptible *)
   175       Unsynchronized.setmp Private_Output.protocol_message_fn
   146 
   176         (fn props => fn body => message Markup.protocolN props body) #>
   147 exception EXIT of exn;
   177       Unsynchronized.setmp print_mode
   148 
   178         ((! print_mode @ protocol_modes1) |> fold (update op =) protocol_modes2);
   149 val crashes = Synchronized.var "Isabelle_Process.crashes" ([]: exn list);
   179 
   150 
   180 
   151 local
   181     (* protocol *)
   152 
   182 
   153 fun recover crash =
   183     fun protocol_loop () =
   154   (Synchronized.change crashes (cons crash);
   184       let
   155     Output.physical_stderr
   185         val continue =
   156       "Recovered from Isabelle process crash -- see also Isabelle_Process.crashes\n");
   186           (case Byte_Message.read_message in_stream of
   157 
   187             NONE => false
   158 fun shutdown () = (Future.shutdown (); ignore (Execution.reset ()));
   188           | SOME [] => (Output.system_message "Isabelle process: no input"; true)
   159 
   189           | SOME (name :: args) => (run_command name args; true))
   160 in
   190           handle EXIT exn => Exn.reraise exn
   161 
   191             | exn => (Runtime.exn_system_message exn handle crash => recover crash; true);
   162 fun loop stream =
   192       in if continue then protocol_loop () else () end;
   163   let
   193 
   164     val continue =
   194     fun protocol () =
   165       (case Byte_Message.read_message stream of
   195      (Session.init_protocol_handlers ();
   166         NONE => false
   196       message Markup.initN [] [XML.Text (Session.welcome ())];
   167       | SOME [] => (Output.system_message "Isabelle process: no input"; true)
   197       protocol_loop ());
   168       | SOME (name :: args) => (run_command name args; true))
   198 
   169       handle EXIT exn => (shutdown (); Exn.reraise exn)
   199     val result = Exn.capture (message_context protocol) ();
   170         | exn => (Runtime.exn_system_message exn handle crash => recover crash; true);
   200 
   171   in if continue then loop stream else shutdown () end;
   201 
   172 
   202     (* shutdown *)
   173 end;
   203 
   174 
   204     val _ = Future.shutdown ();
   175 
   205     val _ = Execution.reset ();
   176 (* init protocol *)
       
   177 
       
   178 val default_modes1 = [Syntax_Trans.no_bracketsN, Syntax_Trans.no_type_bracketsN];
       
   179 val default_modes2 = [isabelle_processN, Pretty.symbolicN];
       
   180 
       
   181 val init_protocol = Thread_Attributes.uninterruptible (fn _ => fn (address, password) =>
       
   182   let
       
   183     val _ = SHA1.test_samples ()
       
   184       handle exn as Fail msg => (Output.physical_stderr (msg ^ "\n"); Exn.reraise exn);
       
   185     val _ = Output.physical_stderr Symbol.STX;
       
   186 
       
   187     val _ = Context.put_generic_context NONE;
       
   188     val _ =
       
   189       Unsynchronized.change print_mode
       
   190         (fn mode => (mode @ default_modes1) |> fold (update op =) default_modes2);
       
   191 
       
   192     val (in_stream, out_stream) = Socket_IO.open_streams address;
       
   193     val _ = Byte_Message.write_line out_stream password;
       
   194     val msg_channel = init_channels out_stream;
       
   195     val _ = loop in_stream;
       
   196     val _ = Message_Channel.shutdown msg_channel;
   206     val _ = Message_Channel.shutdown msg_channel;
   197     val _ = Private_Output.init_channels ();
   207 
   198 
   208   in Exn.release result end);
   199     val _ = print_mode := [];
   209 
   200   in () end);
   210 end;
   201 
   211 
   202 
   212 
   203 (* init options *)
   213 (* init options *)
   204 
   214 
   205 fun init_options () =
   215 fun init_options () =