# HG changeset patch
# User wenzelm
# Date 1476880948 -7200
# Node ID b00508facb4fb5620d29021f3a324c47a5983222
# Parent  c4d16f35c6e72c12cddfc80a0a87137faf9df497
added system option "profiling";

diff -r c4d16f35c6e7 -r b00508facb4f NEWS
--- a/NEWS	Tue Oct 18 17:41:56 2016 +0200
+++ b/NEWS	Wed Oct 19 14:42:28 2016 +0200
@@ -1033,6 +1033,9 @@
 exhaust the small 32-bit address space of the ML process (which is used
 by default).
 
+* System option "profiling" specifies the mode for global ML profiling
+in "isabelle build". Possible values are "time", "allocations".
+
 * System option "ML_process_policy" specifies an optional command prefix
 for the underlying ML process, e.g. to control CPU affinity on
 multiprocessor systems. The "isabelle jedit" tool allows to override the
diff -r c4d16f35c6e7 -r b00508facb4f etc/options
--- a/etc/options	Tue Oct 18 17:41:56 2016 +0200
+++ b/etc/options	Wed Oct 19 14:42:28 2016 +0200
@@ -108,6 +108,9 @@
 option checkpoint : bool = false
   -- "checkpoint for theories during build process (heap compression)"
 
+option profiling : string = ""
+  -- "ML profiling (possible values: time, allocations)"
+
 
 section "ML System"
 
diff -r c4d16f35c6e7 -r b00508facb4f src/Doc/System/Sessions.thy
--- a/src/Doc/System/Sessions.thy	Tue Oct 18 17:41:56 2016 +0200
+++ b/src/Doc/System/Sessions.thy	Wed Oct 19 14:42:28 2016 +0200
@@ -215,6 +215,11 @@
     Isabelle/Scala. Thus it is relatively reliable in canceling processes that
     get out of control, even if there is a deadlock without CPU time usage.
 
+    \<^item> @{system_option_def "profiling"} specifies a mode for global ML
+    profiling. Possible values are the empty string (disabled), \<^verbatim>\<open>time\<close> for
+    @{ML profile_time} and \<^verbatim>\<open>allocations\<close> for @{ML profile_allocations}.
+    Results appear near the bottom of the session log file.
+
   The @{tool_def options} tool prints Isabelle system options. Its
   command-line usage is:
   @{verbatim [display]
diff -r c4d16f35c6e7 -r b00508facb4f src/Pure/Tools/build.ML
--- a/src/Pure/Tools/build.ML	Tue Oct 18 17:41:56 2016 +0200
+++ b/src/Pure/Tools/build.ML	Wed Oct 19 14:42:28 2016 +0200
@@ -114,6 +114,12 @@
           symbols = symbols,
           last_timing = last_timing,
           master_dir = master_dir}
+        |>
+          (case Options.string options "profiling" of
+            "" => I
+          | "time" => profile_time
+          | "allocations" => profile_allocations
+          | bad => error ("Bad profiling option: " ^ quote bad))
         |> Unsynchronized.setmp print_mode
             (space_explode "," (Options.string options "print_mode") @ print_mode_value ())) thys)
     else