diff --git a/src/Pure/General/output.ML b/src/Pure/General/output.ML --- a/src/Pure/General/output.ML +++ b/src/Pure/General/output.ML @@ -1,200 +1,199 @@ (* Title: Pure/General/output.ML Author: Makarius Isabelle output channels. *) signature BASIC_OUTPUT = sig val writeln: string -> unit val tracing: string -> unit val warning: string -> unit val legacy_feature: string -> unit val profile_time: ('a -> 'b) -> 'a -> 'b val profile_time_thread: ('a -> 'b) -> 'a -> 'b val profile_allocations: ('a -> 'b) -> 'a -> 'b end; signature OUTPUT = sig include BASIC_OUTPUT type output = string val default_output: string -> output * int val default_escape: output -> string val add_mode: string -> (string -> output * int) -> (output -> string) -> unit val output_width: string -> output * int val output: string -> output val escape: output -> string val physical_stdout: output -> unit val physical_stderr: output -> unit val physical_writeln: output -> unit type protocol_message_fn = Output_Primitives.protocol_message_fn exception Protocol_Message of Properties.T val protocol_message_undefined: protocol_message_fn val writelns: string list -> unit val state: string -> unit val information: string -> unit val error_message': serial * string -> unit val error_message: string -> unit val system_message: string -> unit val status: string list -> unit val report: string list -> unit val result: Properties.T -> string list -> unit val protocol_message: protocol_message_fn val try_protocol_message: protocol_message_fn end; signature PRIVATE_OUTPUT = sig include OUTPUT val writeln_fn: (output list -> unit) Unsynchronized.ref val state_fn: (output list -> unit) Unsynchronized.ref val information_fn: (output list -> unit) Unsynchronized.ref val tracing_fn: (output list -> unit) Unsynchronized.ref val warning_fn: (output list -> unit) Unsynchronized.ref val legacy_fn: (output list -> unit) Unsynchronized.ref val error_message_fn: (serial * output list -> unit) Unsynchronized.ref val system_message_fn: (output list -> unit) Unsynchronized.ref val status_fn: (output list -> unit) Unsynchronized.ref 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 = struct (** print modes **) type output = string; (*raw system output*) fun default_output s = (s, size s); fun default_escape (s: output) = s; local val default = {output = default_output, escape = default_escape}; val modes = Synchronized.var "Output.modes" (Symtab.make [("", default)]); in fun add_mode name output escape = if Thread_Data.is_virtual then () else Synchronized.change modes (Symtab.update_new (name, {output = output, escape = escape})); fun get_mode () = the_default default (Library.get_first (Symtab.lookup (Synchronized.value modes)) (print_mode_value ())); end; fun output_width x = #output (get_mode ()) x; val output = #1 o output_width; fun escape x = #escape (get_mode ()) x; (** output channels **) (* primitives -- provided via bootstrap environment *) val writeln_fn = Unsynchronized.ref Output_Primitives.writeln_fn; val state_fn = Unsynchronized.ref Output_Primitives.state_fn; val information_fn = Unsynchronized.ref Output_Primitives.information_fn; val tracing_fn = Unsynchronized.ref Output_Primitives.tracing_fn; val warning_fn = Unsynchronized.ref Output_Primitives.warning_fn; val legacy_fn = Unsynchronized.ref Output_Primitives.legacy_fn; val error_message_fn = Unsynchronized.ref Output_Primitives.error_message_fn; val system_message_fn = Unsynchronized.ref Output_Primitives.system_message_fn; val status_fn = Unsynchronized.ref Output_Primitives.status_fn; val report_fn = Unsynchronized.ref Output_Primitives.report_fn; val result_fn = Unsynchronized.ref Output_Primitives.result_fn; type protocol_message_fn = Output_Primitives.protocol_message_fn; val protocol_message_fn = Unsynchronized.ref Output_Primitives.protocol_message_fn; (* physical output -- not to be used in user-space *) fun physical_stdout s = (TextIO.output (TextIO.stdOut, s); TextIO.flushOut TextIO.stdOut); fun physical_stderr s = (TextIO.output (TextIO.stdErr, s); TextIO.flushOut TextIO.stdErr); fun physical_writeln "" = () | physical_writeln s = physical_stdout (suffix "\n" s); (*atomic output!*) (* Isabelle output channels *) exception Protocol_Message of Properties.T; val protocol_message_undefined: Output_Primitives.protocol_message_fn = fn props => fn _ => raise Protocol_Message props; fun init_channels () = (writeln_fn := (physical_writeln o implode); state_fn := (fn ss => ! writeln_fn ss); information_fn := Output_Primitives.ignore_outputs; tracing_fn := (fn ss => ! writeln_fn ss); warning_fn := (physical_writeln o prefix_lines "### " o implode); legacy_fn := (fn ss => ! warning_fn ss); error_message_fn := (fn (_, ss) => physical_writeln (prefix_lines "*** " (implode ss))); system_message_fn := (fn ss => ! writeln_fn ss); status_fn := Output_Primitives.ignore_outputs; report_fn := Output_Primitives.ignore_outputs; result_fn := (fn _ => Output_Primitives.ignore_outputs); protocol_message_fn := protocol_message_undefined); val _ = if Thread_Data.is_virtual then () else init_channels (); fun writelns ss = ! writeln_fn (map output ss); fun writeln s = writelns [s]; fun state s = ! state_fn [output s]; fun information s = ! information_fn [output s]; fun tracing s = ! tracing_fn [output s]; fun warning s = ! warning_fn [output s]; fun legacy_feature s = ! legacy_fn [output ("Legacy feature! " ^ s)]; fun error_message' (i, s) = ! error_message_fn (i, [output s]); fun error_message s = error_message' (serial (), s); fun system_message s = ! system_message_fn [output s]; fun status ss = ! status_fn (map output ss); fun report ss = ! report_fn (map output ss); fun result props ss = ! result_fn props (map output ss); fun protocol_message props body = ! protocol_message_fn props body; fun try_protocol_message props body = protocol_message props body handle Protocol_Message _ => (); (* profiling *) local fun output_profile title entries = let val body = entries |> sort (int_ord o apply2 fst) |> map (fn (count, name) => let val c = string_of_int count; val prefix = replicate_string (Int.max (0, 10 - size c)) " "; in prefix ^ c ^ " " ^ name end); val total = fold (curry (op +) o fst) entries 0; in if total = 0 then () else warning (cat_lines (title :: (body @ ["total: " ^ string_of_int total]))) end; in fun profile_time f x = ML_Profiling.profile_time (output_profile "time profile:") f x; fun profile_time_thread f x = ML_Profiling.profile_time_thread (output_profile "time profile (this thread):") f x; fun profile_allocations f x = ML_Profiling.profile_allocations (output_profile "allocations profile:") f x; end; end; structure Output: OUTPUT = Private_Output; structure Basic_Output: BASIC_OUTPUT = Output; open Basic_Output; diff --git a/src/Pure/System/isabelle_process.ML b/src/Pure/System/isabelle_process.ML --- a/src/Pure/System/isabelle_process.ML +++ b/src/Pure/System/isabelle_process.ML @@ -1,234 +1,244 @@ (* Title: Pure/System/isabelle_process.ML Author: Makarius Isabelle process wrapper. *) signature ISABELLE_PROCESS = sig val is_active: unit -> bool val protocol_command: string -> (string list -> unit) -> unit val reset_tracing: Document_ID.exec -> unit exception EXIT of exn val crashes: exn list Synchronized.var val init_options: unit -> unit val init_options_interactive: unit -> unit val init: unit -> unit end; structure Isabelle_Process: ISABELLE_PROCESS = struct (* print mode *) val isabelle_processN = "isabelle_process"; fun is_active () = Print_Mode.print_mode_active isabelle_processN; 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 *) local val commands = Synchronized.var "Isabelle_Process.commands" (Symtab.empty: (string list -> unit) Symtab.table); in fun protocol_command name cmd = Synchronized.change commands (fn cmds => (if not (Symtab.defined cmds name) then () else warning ("Redefining Isabelle protocol command " ^ quote name); Symtab.update (name, cmd) cmds)); fun run_command name args = (case Symtab.lookup (Synchronized.value commands) name of NONE => error ("Undefined Isabelle protocol command " ^ quote name) | SOME cmd => (Runtime.exn_trace_system (fn () => cmd args) handle _ (*sic!*) => error ("Isabelle protocol command failure: " ^ quote name))); end; (* restricted tracing messages *) val tracing_messages = Synchronized.var "tracing_messages" (Inttab.empty: int Inttab.table); fun reset_tracing exec_id = Synchronized.change tracing_messages (Inttab.delete_safe exec_id); fun update_tracing () = (case Position.parse_id (Position.thread_data ()) of NONE => () | SOME exec_id => let val ok = Synchronized.change_result tracing_messages (fn tab => let val n = the_default 0 (Inttab.lookup tab exec_id) + 1; val limit = Options.default_int "editor_tracing_messages"; val ok = limit <= 0 orelse n <= limit; in (ok, Inttab.update (exec_id, n) tab) end); in if ok then () else let val (text, promise) = Active.dialog_text (); val _ = writeln ("Tracing paused. " ^ text "Stop" ^ ", or continue with next " ^ text "100" ^ ", " ^ text "1000" ^ ", " ^ text "10000" ^ " messages?") val m = Value.parse_int (Future.join promise) handle Fail _ => error "Stopped"; in Synchronized.change tracing_messages (Inttab.map_default (exec_id, 0) (fn k => k - m)) end end); -(* output channels *) +(* init protocol -- uninterruptible *) -val serial_props = Markup.serial_properties o serial; +exception EXIT of exn; -fun init_channels out_stream = +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 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; + + + (* 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 = Message_Channel.send msg_channel (Message_Channel.message name props body); fun standard_message props name ss = if forall (fn s => s = "") ss then () else let val props' = (case (Properties.defined props Markup.idN, Position.get_id (Position.thread_data ())) of (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); - Session.init_protocol_handlers (); - message Markup.initN [] [XML.Text (Session.welcome ())]; - msg_channel - end; + val serial_props = Markup.serial_properties o serial; + + 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); - -local - -fun recover crash = - (Synchronized.change crashes (cons crash); - Output.physical_stderr - "Recovered from Isabelle process crash -- see also Isabelle_Process.crashes\n"); + (* protocol *) -fun shutdown () = (Future.shutdown (); ignore (Execution.reset ())); - -in + 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 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; + fun protocol () = + (Session.init_protocol_handlers (); + message Markup.initN [] [XML.Text (Session.welcome ())]; + protocol_loop ()); + + val result = Exn.capture (message_context protocol) (); + + + (* 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 () = (ML_Print_Depth.set_print_depth (Options.default_int "ML_print_depth"); Future.ML_statistics := Options.default_bool "ML_statistics"; Multithreading.trace := Options.default_int "threads_trace"; Multithreading.max_threads_update (Options.default_int "threads"); Multithreading.parallel_proofs := Options.default_int "parallel_proofs"; if Options.default_bool "export_standard_proofs" then Proofterm.proofs := 2 else (); let val proofs = Options.default_int "record_proofs" in if proofs < 0 then () else Proofterm.proofs := proofs end; Printer.show_markup_default := false); fun init_options_interactive () = (init_options (); Multithreading.parallel_proofs := (if Options.default_int "parallel_proofs" > 0 then 3 else 0); Printer.show_markup_default := true); (* generic init *) fun init () = let val address = Options.default_string \<^system_option>\system_channel_address\; val password = Options.default_string \<^system_option>\system_channel_password\; in if address <> "" andalso password <> "" then init_protocol (address, password) else init_options () end; end;