# HG changeset patch # User wenzelm # Date 1585742130 -7200 # Node ID 60659474ed36635af8ffac8fa5ee2b06c66a8893 # Parent 43ba9fece20dcfda90aa7efe8b4edc08241c872f traditional print_mode for batch build; diff -r 43ba9fece20d -r 60659474ed36 src/Pure/System/isabelle_process.ML --- a/src/Pure/System/isabelle_process.ML Wed Apr 01 12:59:05 2020 +0200 +++ b/src/Pure/System/isabelle_process.ML Wed Apr 01 13:55:30 2020 +0200 @@ -14,6 +14,7 @@ val init_options: unit -> unit val init_options_interactive: unit -> unit val init: unit -> unit + val init_build: unit -> unit end; structure Isabelle_Process: ISABELLE_PROCESS = @@ -110,7 +111,7 @@ in -val init_protocol = Thread_Attributes.uninterruptible (fn _ => fn (address, password) => +fun init_protocol modes = 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); @@ -173,7 +174,7 @@ 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); + ((! print_mode @ #1 modes) |> fold (update op =) (#2 modes)); (* protocol *) @@ -231,14 +232,17 @@ (* generic init *) -fun init () = +fun init_modes modes = 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) + then init_protocol modes (address, password) else init_options () end; +fun init () = init_modes (protocol_modes1, protocol_modes2); +fun init_build () = init_modes ([], protocol_modes2); + end; diff -r 43ba9fece20d -r 60659474ed36 src/Pure/Tools/build.scala --- a/src/Pure/Tools/build.scala Wed Apr 01 12:59:05 2020 +0200 +++ b/src/Pure/Tools/build.scala Wed Apr 01 13:55:30 2020 +0200 @@ -258,7 +258,7 @@ val handler = new Handler(progress, session, name) session.init_protocol_handler(handler) - val eval_main = Command_Line.ML_tool("Isabelle_Process.init ()" :: eval_store) + val eval_main = Command_Line.ML_tool("Isabelle_Process.init_build ()" :: eval_store) val process = Isabelle_Process(session, options, sessions_structure, store,