8 sig |
8 sig |
9 val is_active: unit -> bool |
9 val is_active: unit -> bool |
10 val protocol_command: string -> (string list -> unit) -> unit |
10 val protocol_command: string -> (string list -> unit) -> unit |
11 val reset_tracing: Document_ID.exec -> unit |
11 val reset_tracing: Document_ID.exec -> unit |
12 val crashes: exn list Synchronized.var |
12 val crashes: exn list Synchronized.var |
13 val init_protocol: string -> unit |
|
14 val init_options: unit -> unit |
13 val init_options: unit -> unit |
15 val init_options_interactive: unit -> unit |
14 val init_options_interactive: unit -> unit |
|
15 val init: unit -> unit |
16 end; |
16 end; |
17 |
17 |
18 structure Isabelle_Process: ISABELLE_PROCESS = |
18 structure Isabelle_Process: ISABELLE_PROCESS = |
19 struct |
19 struct |
20 |
20 |
171 (* init protocol *) |
171 (* init protocol *) |
172 |
172 |
173 val default_modes1 = [Syntax_Trans.no_bracketsN, Syntax_Trans.no_type_bracketsN]; |
173 val default_modes1 = [Syntax_Trans.no_bracketsN, Syntax_Trans.no_type_bracketsN]; |
174 val default_modes2 = [isabelle_processN, Pretty.symbolicN]; |
174 val default_modes2 = [isabelle_processN, Pretty.symbolicN]; |
175 |
175 |
176 val init_protocol = Thread_Attributes.uninterruptible (fn _ => fn socket => |
176 val init_protocol = Thread_Attributes.uninterruptible (fn _ => fn (address, password) => |
177 let |
177 let |
178 val _ = SHA1.test_samples () |
178 val _ = SHA1.test_samples () |
179 handle exn as Fail msg => (Output.physical_stderr (msg ^ "\n"); Exn.reraise exn); |
179 handle exn as Fail msg => (Output.physical_stderr (msg ^ "\n"); Exn.reraise exn); |
180 val _ = Output.physical_stderr Symbol.STX; |
180 val _ = Output.physical_stderr Symbol.STX; |
181 |
181 |
182 val _ = Context.put_generic_context NONE; |
182 val _ = Context.put_generic_context NONE; |
183 val _ = |
183 val _ = |
184 Unsynchronized.change print_mode |
184 Unsynchronized.change print_mode |
185 (fn mode => (mode @ default_modes1) |> fold (update op =) default_modes2); |
185 (fn mode => (mode @ default_modes1) |> fold (update op =) default_modes2); |
186 |
186 |
187 val (in_stream, out_stream) = Socket_IO.open_streams socket; |
187 val (in_stream, out_stream) = Socket_IO.open_streams address; |
|
188 val _ = Byte_Message.write_line out_stream password; |
188 val msg_channel = init_channels out_stream; |
189 val msg_channel = init_channels out_stream; |
189 val _ = loop in_stream; |
190 val _ = loop in_stream; |
190 val _ = Message_Channel.shutdown msg_channel; |
191 val _ = Message_Channel.shutdown msg_channel; |
191 val _ = Private_Output.init_channels (); |
192 val _ = Private_Output.init_channels (); |
192 |
193 |
209 fun init_options_interactive () = |
210 fun init_options_interactive () = |
210 (init_options (); |
211 (init_options (); |
211 Multithreading.parallel_proofs := (if Options.default_int "parallel_proofs" > 0 then 3 else 0); |
212 Multithreading.parallel_proofs := (if Options.default_int "parallel_proofs" > 0 then 3 else 0); |
212 Printer.show_markup_default := true); |
213 Printer.show_markup_default := true); |
213 |
214 |
214 end; |
215 |
|
216 (* generic init *) |
|
217 |
|
218 fun init () = |
|
219 let |
|
220 val address = Options.default_string \<^system_option>\<open>system_channel_address\<close>; |
|
221 val password = Options.default_string \<^system_option>\<open>system_channel_password\<close>; |
|
222 in |
|
223 if address <> "" andalso password <> "" |
|
224 then init_protocol (address, password) |
|
225 else init_options () |
|
226 end; |
|
227 |
|
228 end; |