# HG changeset patch
# User wenzelm
# Date 1450711835 -3600
# Node ID 4fec637b72f24d4b9b22f8594bef423ae31789b2
# Parent  b4bfa62e799dcc7d26e5d2f4899f1a9e25a161d8# Parent  5a9a85c4cfb3e648167ab41606087e20a811aad4
merged

diff -r b4bfa62e799d -r 4fec637b72f2 NEWS
--- a/NEWS	Mon Dec 21 14:44:44 2015 +0100
+++ b/NEWS	Mon Dec 21 16:30:35 2015 +0100
@@ -669,6 +669,13 @@
 tools, but can also cause INCOMPATIBILITY for tools that don't observe
 the proof context discipline.
 
+* The following combinators for low-level profiling of the ML runtime
+system are available:
+
+  profile_time          (*CPU time*)
+  profile_time_thread   (*CPU time on this thread*)
+  profile_allocations   (*overall heap allocations*)
+
 
 *** System ***
 
diff -r b4bfa62e799d -r 4fec637b72f2 src/Pure/General/output.ML
--- a/src/Pure/General/output.ML	Mon Dec 21 14:44:44 2015 +0100
+++ b/src/Pure/General/output.ML	Mon Dec 21 16:30:35 2015 +0100
@@ -10,6 +10,9 @@
   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 =
@@ -131,6 +134,40 @@
 fun protocol_message props ss = ! protocol_message_fn props (map output ss);
 fun try_protocol_message props ss = protocol_message props ss 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 Basic_Output: BASIC_OUTPUT = Output;
diff -r b4bfa62e799d -r 4fec637b72f2 src/Pure/General/pretty.ML
--- a/src/Pure/General/pretty.ML	Mon Dec 21 14:44:44 2015 +0100
+++ b/src/Pure/General/pretty.ML	Mon Dec 21 16:30:35 2015 +0100
@@ -118,11 +118,22 @@
   | length (Break (_, wd, _)) = wd
   | length (Str (_, len)) = len;
 
-fun body_length [] len = len
-  | body_length (e :: es) len = body_length es (length e + len);
+fun make_block markup consistent indent body =
+  let
+    fun body_length prts len =
+      let
+        val (line, rest) = take_prefix (fn Break (true, _, _) => false | _ => true) prts;
+        val len' = Int.max (fold (Integer.add o length) line 0, len);
+      in
+        (case rest of
+          Break (true, _, ind) :: rest' =>
+            body_length (Break (false, indent + ind, 0) :: rest') len'
+        | [] => len')
+      end;
+  in Block (markup, consistent, indent, body, body_length body 0) end;
 
-fun make_block m consistent indent es = Block (m, consistent, indent, es, body_length es 0);
-fun markup_block m indent es = make_block (Markup.output m) false indent es;
+fun markup_block markup indent es =
+  make_block (Markup.output markup) false indent es;
 
 
 
diff -r b4bfa62e799d -r 4fec637b72f2 src/Pure/General/pretty.scala
--- a/src/Pure/General/pretty.scala	Mon Dec 21 14:44:44 2015 +0100
+++ b/src/Pure/General/pretty.scala	Mon Dec 21 16:30:35 2015 +0100
@@ -63,7 +63,20 @@
       consistent: Boolean,
       indent: Int,
       body: List[Tree]): Tree =
-    Block(markup, consistent, indent, body, (0.0 /: body) { case (n, t) => n + t.length })
+  {
+    def body_length(prts: List[Tree], len: Double): Double =
+    {
+      val (line, rest) =
+        Library.take_prefix[Tree]({ case Break(true, _, _) => false case _ => true }, prts)
+      val len1 = ((0.0 /: line) { case (l, t) => l + t.length }) max len
+      rest match {
+        case Break(true, _, ind) :: rest1 =>
+          body_length(Break(false, indent + ind, 0) :: rest1, len1)
+        case Nil => len1
+      }
+    }
+    Block(markup, consistent, indent, body, body_length(body, 0.0))
+  }
 
 
   /* formatted output */
diff -r b4bfa62e799d -r 4fec637b72f2 src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Mon Dec 21 14:44:44 2015 +0100
+++ b/src/Pure/Isar/toplevel.ML	Mon Dec 21 16:30:35 2015 +0100
@@ -26,7 +26,6 @@
   val pretty_state: state -> Pretty.T list
   val string_of_state: state -> string
   val pretty_abstract: state -> Pretty.T
-  val profiling: int Unsynchronized.ref
   type transition
   val empty: transition
   val name_of: transition -> string
@@ -204,9 +203,6 @@
 
 (** toplevel transitions **)
 
-val profiling = Unsynchronized.ref 0;
-
-
 (* node transactions -- maintaining stable checkpoints *)
 
 exception FAILURE of state * exn;
@@ -568,10 +564,7 @@
   setmp_thread_position tr (fn state =>
     let
       val timing_start = Timing.start ();
-
-      val (result, opt_err) =
-         state |> (apply_trans int trans |> ! profiling > 0 ? profile (! profiling));
-
+      val (result, opt_err) = apply_trans int trans state;
       val timing_result = Timing.result timing_start;
       val timing_props =
         Markup.command_timing :: (Markup.nameN, name_of tr) :: Position.properties_of (pos_of tr);
diff -r b4bfa62e799d -r 4fec637b72f2 src/Pure/ML-Systems/ml_debugger.ML
--- a/src/Pure/ML-Systems/ml_debugger.ML	Mon Dec 21 14:44:44 2015 +0100
+++ b/src/Pure/ML-Systems/ml_debugger.ML	Mon Dec 21 16:30:35 2015 +0100
@@ -21,6 +21,7 @@
   val debug_function_result: state -> ML_Name_Space.valueVal
   val debug_location: state -> 'location
   val debug_name_space: state -> ML_Name_Space.T
+  val debug_local_name_space: state -> ML_Name_Space.T
 end;
 
 structure ML_Debugger: ML_DEBUGGER =
@@ -58,5 +59,6 @@
 fun debug_function_result () = fail ();
 fun debug_location () = fail ();
 fun debug_name_space () = fail ();
+fun debug_local_name_space () = fail ();
 
 end;
diff -r b4bfa62e799d -r 4fec637b72f2 src/Pure/ML-Systems/ml_debugger_polyml-5.6.ML
--- a/src/Pure/ML-Systems/ml_debugger_polyml-5.6.ML	Mon Dec 21 14:44:44 2015 +0100
+++ b/src/Pure/ML-Systems/ml_debugger_polyml-5.6.ML	Mon Dec 21 16:30:35 2015 +0100
@@ -22,6 +22,7 @@
   val debug_function_result: state -> ML_Name_Space.valueVal
   val debug_location: state -> location
   val debug_name_space: state -> ML_Name_Space.T
+  val debug_local_name_space: state -> ML_Name_Space.T
 end;
 
 structure ML_Debugger: ML_DEBUGGER =
@@ -66,5 +67,6 @@
 val debug_function_result = PolyML.DebuggerInterface.debugFunctionResult;
 val debug_location = PolyML.DebuggerInterface.debugLocation;
 val debug_name_space = PolyML.DebuggerInterface.debugNameSpace;
+val debug_local_name_space = PolyML.DebuggerInterface.debugLocalNameSpace;
 
 end;
diff -r b4bfa62e799d -r 4fec637b72f2 src/Pure/ML-Systems/ml_profiling_polyml-5.6.ML
--- a/src/Pure/ML-Systems/ml_profiling_polyml-5.6.ML	Mon Dec 21 14:44:44 2015 +0100
+++ b/src/Pure/ML-Systems/ml_profiling_polyml-5.6.ML	Mon Dec 21 16:30:35 2015 +0100
@@ -4,14 +4,16 @@
 Profiling for Poly/ML 5.6.
 *)
 
-fun profile 0 f x = f x
-  | profile n f x =
-      let
-        val mode =
-          (case n of
-            1 => PolyML.Profiling.ProfileTime
-          | 2 => PolyML.Profiling.ProfileAllocations
-          | 3 => PolyML.Profiling.ProfileLongIntEmulation
-          | 6 => PolyML.Profiling.ProfileTimeThisThread
-          | _ => raise Fail ("Bad profile mode: " ^ Int.toString n));
-      in PolyML.Profiling.profile mode f x end;
+structure ML_Profiling =
+struct
+
+fun profile_time pr f x =
+  PolyML.Profiling.profileStream pr PolyML.Profiling.ProfileTime f x;
+
+fun profile_time_thread pr f x =
+  PolyML.Profiling.profileStream pr PolyML.Profiling.ProfileTimeThisThread f x;
+
+fun profile_allocations pr f x =
+  PolyML.Profiling.profileStream pr PolyML.Profiling.ProfileAllocations f x;
+
+end;
diff -r b4bfa62e799d -r 4fec637b72f2 src/Pure/ML-Systems/ml_profiling_polyml.ML
--- a/src/Pure/ML-Systems/ml_profiling_polyml.ML	Mon Dec 21 14:44:44 2015 +0100
+++ b/src/Pure/ML-Systems/ml_profiling_polyml.ML	Mon Dec 21 16:30:35 2015 +0100
@@ -4,10 +4,24 @@
 Profiling for Poly/ML.
 *)
 
-fun profile 0 f x = f x
-  | profile n f x =
-      let
-        val _ = RunCall.run_call1 RuntimeCalls.POLY_SYS_profiler n;
-        val res = Exn.capture f x;
-        val _ = RunCall.run_call1 RuntimeCalls.POLY_SYS_profiler 0;
-      in Exn.release res end;
+structure ML_Profiling =
+struct
+
+local
+
+fun profile n f x =
+  let
+    val _ = RunCall.run_call1 RuntimeCalls.POLY_SYS_profiler n;
+    val res = Exn.capture f x;
+    val _ = RunCall.run_call1 RuntimeCalls.POLY_SYS_profiler 0;
+  in Exn.release res end;
+
+in
+
+fun profile_time (_: (int * string) list -> unit) f x = profile 1 f x;
+fun profile_time_thread (_: (int * string) list -> unit) f x = profile 6 f x;
+fun profile_allocations (_: (int * string) list -> unit) f x = profile 2 f x;
+
+end;
+
+end;
diff -r b4bfa62e799d -r 4fec637b72f2 src/Pure/ML-Systems/smlnj.ML
--- a/src/Pure/ML-Systems/smlnj.ML	Mon Dec 21 14:44:44 2015 +0100
+++ b/src/Pure/ML-Systems/smlnj.ML	Mon Dec 21 16:30:35 2015 +0100
@@ -74,7 +74,12 @@
   (Control.primaryPrompt := p1; Control.secondaryPrompt := p2);
 
 (*dummy implementation*)
-fun profile (n: int) f x = f x;
+structure ML_Profiling =
+struct
+  fun profile_time (_: (int * string) list -> unit) f x = f x;
+  fun profile_time_thread (_: (int * string) list -> unit) f x = f x;
+  fun profile_allocations (_: (int * string) list -> unit) f x = f x;
+end;
 
 (*dummy implementation*)
 fun print_exception_trace (_: exn -> string) (_: string -> unit) f = f ();
diff -r b4bfa62e799d -r 4fec637b72f2 src/Pure/Tools/debugger.ML
--- a/src/Pure/Tools/debugger.ML	Mon Dec 21 14:44:44 2015 +0100
+++ b/src/Pure/Tools/debugger.ML	Mon Dec 21 16:30:35 2015 +0100
@@ -191,7 +191,7 @@
     fun print x =
       Pretty.from_ML (ML_Name_Space.display_val (x, ML_Options.get_print_depth (), space));
     fun print_all () =
-      #allVal (ML_Debugger.debug_name_space (the_debug_state thread_name index)) ()
+      #allVal (ML_Debugger.debug_local_name_space (the_debug_state thread_name index)) ()
       |> sort_by #1 |> map (Pretty.item o single o print o #2)
       |> Pretty.chunks |> Pretty.string_of |> writeln_message;
   in Context.setmp_thread_data (SOME context) print_all () end;
diff -r b4bfa62e799d -r 4fec637b72f2 src/Pure/library.scala
--- a/src/Pure/library.scala	Mon Dec 21 14:44:44 2015 +0100
+++ b/src/Pure/library.scala	Mon Dec 21 16:30:35 2015 +0100
@@ -205,7 +205,10 @@
     try { Some(new Regex(s)) } catch { case ERROR(_) => None }
 
 
-  /* canonical list operations */
+  /* lists */
+
+  def take_prefix[A](pred: A => Boolean, xs: List[A]): (List[A], List[A]) =
+    (xs.takeWhile(pred), xs.dropWhile(pred))
 
   def member[A, B](xs: List[A])(x: B): Boolean = xs.contains(x)
   def insert[A](x: A)(xs: List[A]): List[A] = if (xs.contains(x)) xs else x :: xs