src/Pure/Tools/build.ML
changeset 72019 940195fbb282
parent 72012 c81e58a81b8c
child 72103 7b318273a4aa
equal deleted inserted replaced
72018:5c9984820caa 72019:940195fbb282
    44   |> the_default Time.zeroTime;
    44   |> the_default Time.zeroTime;
    45 
    45 
    46 
    46 
    47 (* session timing *)
    47 (* session timing *)
    48 
    48 
    49 fun session_timing session_name verbose f x =
    49 fun session_timing f x =
    50   let
    50   let
    51     val start = Timing.start ();
    51     val start = Timing.start ();
    52     val y = f x;
    52     val y = f x;
    53     val timing = Timing.result start;
    53     val timing = Timing.result start;
    54 
    54 
    55     val threads = string_of_int (Multithreading.max_threads ());
    55     val threads = string_of_int (Multithreading.max_threads ());
    56     val factor = Time.toReal (#cpu timing) / Time.toReal (#elapsed timing)
    56     val props = [("threads", threads)] @ Markup.timing_properties timing;
    57       |> Real.fmt (StringCvt.FIX (SOME 2));
    57     val _ = Output.protocol_message (Markup.session_timing :: props) [];
    58 
       
    59     val timing_props = [("threads", threads)] @ Markup.timing_properties timing;
       
    60     val _ = Output.protocol_message (Markup.session_timing :: timing_props) [];
       
    61     val _ =
       
    62       if verbose then
       
    63         Output.physical_stderr ("Timing " ^ session_name ^ " (" ^
       
    64           threads ^ " threads, " ^ Timing.message timing ^ ", factor " ^ factor ^ ")\n")
       
    65       else ();
       
    66   in y end;
    58   in y end;
    67 
    59 
    68 
    60 
    69 (* protocol messages *)
    61 (* protocol messages *)
    70 
    62 
   209     val last_timing = get_timings (fold update_timings command_timings empty_timings);
   201     val last_timing = get_timings (fold update_timings command_timings empty_timings);
   210 
   202 
   211     val res1 =
   203     val res1 =
   212       theories |>
   204       theories |>
   213         (List.app (build_theories symbols bibtex_entries last_timing session_name master_dir)
   205         (List.app (build_theories symbols bibtex_entries last_timing session_name master_dir)
   214           |> session_timing session_name verbose
   206           |> session_timing
   215           |> Exn.capture);
   207           |> Exn.capture);
   216     val res2 = Exn.capture Session.finish ();
   208     val res2 = Exn.capture Session.finish ();
   217 
   209 
   218     val _ = Resources.finish_session_base ();
   210     val _ = Resources.finish_session_base ();
   219     val _ = Par_Exn.release_all [res1, res2];
   211     val _ = Par_Exn.release_all [res1, res2];