traditional print_mode for batch build;
authorwenzelm
Wed, 01 Apr 2020 13:55:30 +0200
changeset 71859 60659474ed36
parent 71858 43ba9fece20d
child 71860 07e6053ce89c
traditional print_mode for batch build;
src/Pure/System/isabelle_process.ML
src/Pure/Tools/build.scala
--- 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>\<open>system_channel_address\<close>;
     val password = Options.default_string \<^system_option>\<open>system_channel_password\<close>;
   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;
--- 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,