src/Pure/Tools/build.ML
changeset 58928 23d0ffd48006
parent 58849 ef7700ecce83
child 59058 a78612c67ec0
equal deleted inserted replaced
58927:cf47382db395 58928:23d0ffd48006
   155 
   155 
   156       val res1 =
   156       val res1 =
   157         theories |>
   157         theories |>
   158           (List.app (use_theories_condition last_timing)
   158           (List.app (use_theories_condition last_timing)
   159             |> session_timing name verbose
   159             |> session_timing name verbose
   160             |> Unsynchronized.setmp Outer_Syntax.batch_mode true
       
   161             |> Unsynchronized.setmp Output.protocol_message_fn protocol_message
   160             |> Unsynchronized.setmp Output.protocol_message_fn protocol_message
   162             |> Multithreading.max_threads_setmp (Options.int options "threads")
   161             |> Multithreading.max_threads_setmp (Options.int options "threads")
   163             |> Exn.capture);
   162             |> Exn.capture);
   164       val res2 = Exn.capture Session.finish ();
   163       val res2 = Exn.capture Session.finish ();
   165       val _ = Par_Exn.release_all [res1, res2];
   164       val _ = Par_Exn.release_all [res1, res2];