# HG changeset patch # User wenzelm # Date 1623076826 -7200 # Node ID 364bac6691dee476ca3515a3c686711865290168 # Parent 5153fad491f36484fa16b2b9ecc7f23ce7e29242 clarified modules; diff -r 5153fad491f3 -r 364bac6691de src/Pure/General/output.ML --- a/src/Pure/General/output.ML Mon Jun 07 15:13:34 2021 +0200 +++ b/src/Pure/General/output.ML Mon Jun 07 16:40:26 2021 +0200 @@ -10,9 +10,6 @@ val tracing: string -> unit val warning: string -> unit val legacy_feature: string -> unit - val profile_time: ('a -> 'b) -> 'a -> 'b - val profile_time_thread: ('a -> 'b) -> 'a -> 'b - val profile_allocations: ('a -> 'b) -> 'a -> 'b end; signature OUTPUT = @@ -158,40 +155,6 @@ fun protocol_message props body = ! protocol_message_fn props body; fun try_protocol_message props body = protocol_message props body handle Protocol_Message _ => (); - -(* profiling *) - -local - -fun output_profile title entries = - let - val body = entries - |> sort (int_ord o apply2 fst) - |> map (fn (count, name) => - let - val c = string_of_int count; - val prefix = replicate_string (Int.max (0, 10 - size c)) " "; - in prefix ^ c ^ " " ^ name end); - val total = fold (curry (op +) o fst) entries 0; - in - if total = 0 then () - else warning (cat_lines (title :: (body @ ["total: " ^ string_of_int total]))) - end; - -in - -fun profile_time f x = - ML_Profiling.profile_time (output_profile "time profile:") f x; - -fun profile_time_thread f x = - ML_Profiling.profile_time_thread (output_profile "time profile (this thread):") f x; - -fun profile_allocations f x = - ML_Profiling.profile_allocations (output_profile "allocations profile:") f x; - -end; - - end; structure Output: OUTPUT = Private_Output; diff -r 5153fad491f3 -r 364bac6691de src/Pure/ML/ml_profiling.ML --- a/src/Pure/ML/ml_profiling.ML Mon Jun 07 15:13:34 2021 +0200 +++ b/src/Pure/ML/ml_profiling.ML Mon Jun 07 16:40:26 2021 +0200 @@ -6,21 +6,39 @@ signature ML_PROFILING = sig - val profile_time: ((int * string) list -> unit) -> ('a -> 'b) -> 'a -> 'b - val profile_time_thread: ((int * string) list -> unit) -> ('a -> 'b) -> 'a -> 'b - val profile_allocations: ((int * string) list -> unit) -> ('a -> 'b) -> 'a -> 'b + val profile_time: ('a -> 'b) -> 'a -> 'b + val profile_time_thread: ('a -> 'b) -> 'a -> 'b + val profile_allocations: ('a -> 'b) -> 'a -> 'b end; structure ML_Profiling: ML_PROFILING = struct -fun profile_time pr f x = - PolyML.Profiling.profileStream pr PolyML.Profiling.ProfileTime f x; +fun profile mode title = + mode |> PolyML.Profiling.profileStream (fn entries => + let + val body = entries + |> sort (int_ord o apply2 fst) + |> map (fn (count, name) => + let + val c = string_of_int count; + val prefix = replicate_string (Int.max (0, 10 - size c)) " "; + in prefix ^ c ^ " " ^ name end); + val total = fold (curry (op +) o fst) entries 0; + in + if total = 0 then () + else warning (cat_lines (title :: (body @ ["total: " ^ string_of_int total]))) + end); -fun profile_time_thread pr f x = - PolyML.Profiling.profileStream pr PolyML.Profiling.ProfileTimeThisThread f x; +fun profile_time f = + profile PolyML.Profiling.ProfileTime "time profile:" f; -fun profile_allocations pr f x = - PolyML.Profiling.profileStream pr PolyML.Profiling.ProfileAllocations f x; +fun profile_time_thread f = + profile PolyML.Profiling.ProfileTimeThisThread "time profile (this thread):" f; + +fun profile_allocations f = + profile PolyML.Profiling.ProfileAllocations "allocations profile:" f; end; + +open ML_Profiling; diff -r 5153fad491f3 -r 364bac6691de src/Pure/ROOT.ML --- a/src/Pure/ROOT.ML Mon Jun 07 15:13:34 2021 +0200 +++ b/src/Pure/ROOT.ML Mon Jun 07 16:40:26 2021 +0200 @@ -27,7 +27,6 @@ ML_file "Concurrent/counter.ML"; ML_file "ML/ml_heap.ML"; -ML_file "ML/ml_profiling.ML"; ML_file "ML/ml_print_depth0.ML"; ML_file "ML/ml_pretty.ML"; ML_file "ML/ml_compiler0.ML"; @@ -47,6 +46,7 @@ ML_file "General/properties.ML"; ML_file "General/output.ML"; ML_file "PIDE/markup.ML"; +ML_file "ML/ml_profiling.ML"; ML_file "General/utf8.ML"; ML_file "General/scan.ML"; ML_file "General/source.ML";