equal
deleted
inserted
replaced
94 |
94 |
95 val threads = string_of_int (Multithreading.max_threads_value ()); |
95 val threads = string_of_int (Multithreading.max_threads_value ()); |
96 val factor = Time.toReal (#cpu timing) / Time.toReal (#elapsed timing) |
96 val factor = Time.toReal (#cpu timing) / Time.toReal (#elapsed timing) |
97 |> Real.fmt (StringCvt.FIX (SOME 2)); |
97 |> Real.fmt (StringCvt.FIX (SOME 2)); |
98 |
98 |
99 val _ = |
99 val timing_props = |
100 writeln ("\fTiming = " ^ ML_Syntax.print_properties |
100 [("threads", threads)] @ Markup.timing_properties timing @ [("factor", factor)]; |
101 ([("threads", threads)] @ Markup.timing_properties timing @ [("factor", factor)])); |
101 val _ = writeln ("\fTiming = " ^ YXML.string_of_body (XML.Encode.properties timing_props)); |
102 val _ = |
102 val _ = |
103 if verbose then |
103 if verbose then |
104 Output.physical_stderr ("Timing " ^ name ^ " (" ^ |
104 Output.physical_stderr ("Timing " ^ name ^ " (" ^ |
105 threads ^ " threads, " ^ Timing.message timing ^ ", factor " ^ factor ^ ")\n") |
105 threads ^ " threads, " ^ Timing.message timing ^ ", factor " ^ factor ^ ")\n") |
106 else (); |
106 else (); |