merged

--- a/src/Pure/Admin/build_status.scala	Sat Feb 23 19:50:21 2019 +0000
+++ b/src/Pure/Admin/build_status.scala	Sat Feb 23 21:51:40 2019 +0100
@@ -116,6 +116,10 @@
           "ml_timing_elapsed",
           "ml_timing_cpu",
           "ml_timing_gc",
+          "maximum_code",
+          "average_code",
+          "maximum_stack",
+          "average_stack",
           "maximum_heap",
           "average_heap",
           "stored_heap",
@@ -135,6 +139,10 @@
             entry.ml_timing.elapsed.ms,
             entry.ml_timing.cpu.ms,
             entry.ml_timing.gc.ms,
+            entry.maximum_code,
+            entry.average_code,
+            entry.maximum_stack,
+            entry.average_stack,
             entry.maximum_heap,
             entry.average_heap,
             entry.stored_heap,
@@ -151,6 +159,10 @@
     afp_version: String,
     timing: Timing,
     ml_timing: Timing,
+    maximum_code: Long,
+    average_code: Long,
+    maximum_stack: Long,
+    average_stack: Long,
     maximum_heap: Long,
     average_heap: Long,
     stored_heap: Long,
@@ -299,9 +311,13 @@
                     Build_Log.Data.ml_timing_elapsed,
                     Build_Log.Data.ml_timing_cpu,
                     Build_Log.Data.ml_timing_gc),
-                maximum_heap = ml_stats.maximum_heap_size,
-                average_heap = ml_stats.average_heap_size,
-                stored_heap = ML_Statistics.heap_scale(res.long(Build_Log.Data.heap_size)),
+                maximum_code = ml_stats.maximum(ML_Statistics.CODE_SIZE).toLong,
+                average_code = ml_stats.average(ML_Statistics.CODE_SIZE).toLong,
+                maximum_stack = ml_stats.maximum(ML_Statistics.STACK_SIZE).toLong,
+                average_stack = ml_stats.average(ML_Statistics.STACK_SIZE).toLong,
+                maximum_heap = ml_stats.maximum(ML_Statistics.HEAP_SIZE).toLong,
+                average_heap = ml_stats.average(ML_Statistics.HEAP_SIZE).toLong,
+                stored_heap = ML_Statistics.mem_scale(res.long(Build_Log.Data.heap_size)),
                 status = Build_Log.Session_Status.withName(res.string(Build_Log.Data.status)),
                 errors =
                   Build_Log.uncompress_errors(res.bytes(Build_Log.Data.errors),
@@ -353,9 +369,6 @@
     def clean_name(name: String): String =
       name.flatMap(c => if (c == ' ' || c == '/') "_" else if (c == ',') "" else c.toString)
 
-    def print_heap(x: Long): Option[String] =
-      if (x == 0L) None else Some(x.toString + " M")
-
     HTML.write_document(target_dir, "index.html",
       List(HTML.title("Isabelle build status")),
       List(HTML.chapter("Isabelle build status"),
@@ -409,7 +422,11 @@
                       entry.timing.resources.minutes,
                       entry.ml_timing.elapsed.minutes,
                       entry.ml_timing.resources.minutes,
-                      entry.maximum_heap,
+                      entry.maximum_code,
+                      entry.maximum_code,
+                      entry.average_stack,
+                      entry.maximum_stack,
+                      entry.average_heap,
                       entry.average_heap,
                       entry.stored_heap).mkString(" "))))
 
@@ -466,12 +483,12 @@
 
               val heap_plots =
                 List(
-                  """ using 1:6 smooth sbezier title "maximum heap (smooth)" """,
-                  """ using 1:6 smooth csplines title "maximum heap" """,
-                  """ using 1:7 smooth sbezier title "average heap (smooth)" """,
-                  """ using 1:7 smooth csplines title "average heap" """,
-                  """ using 1:8 smooth sbezier title "stored heap (smooth)" """,
-                  """ using 1:8 smooth csplines title "stored heap" """)
+                  """ using 1:6 smooth sbezier title "heap maximum (smooth)" """,
+                  """ using 1:6 smooth csplines title "heap maximum" """,
+                  """ using 1:7 smooth sbezier title "heap average (smooth)" """,
+                  """ using 1:7 smooth csplines title "heap average" """,
+                  """ using 1:8 smooth sbezier title "heap stored (smooth)" """,
+                  """ using 1:8 smooth csplines title "heap stored" """)
 
               def jfreechart(plot_name: String, fields: ML_Statistics.Fields): Image =
               {
@@ -530,12 +547,20 @@
                     List(HTML.link(data_files(session.name).file_name, HTML.text("CSV"))),
                   HTML.text("timing:") -> HTML.text(session.head.timing.message_resources),
                   HTML.text("ML timing:") -> HTML.text(session.head.ml_timing.message_resources)) :::
-                print_heap(session.head.maximum_heap).map(s =>
-                  HTML.text("maximum heap:") -> HTML.text(s)).toList :::
-                print_heap(session.head.average_heap).map(s =>
-                  HTML.text("average heap:") -> HTML.text(s)).toList :::
-                print_heap(session.head.stored_heap).map(s =>
-                  HTML.text("stored heap:") -> HTML.text(s)).toList :::
+                ML_Statistics.mem_print(session.head.maximum_code).map(s =>
+                  HTML.text("code maximum:") -> HTML.text(s)).toList :::
+                ML_Statistics.mem_print(session.head.average_code).map(s =>
+                  HTML.text("code average:") -> HTML.text(s)).toList :::
+                ML_Statistics.mem_print(session.head.maximum_stack).map(s =>
+                  HTML.text("stack maximum:") -> HTML.text(s)).toList :::
+                ML_Statistics.mem_print(session.head.average_stack).map(s =>
+                  HTML.text("stack average:") -> HTML.text(s)).toList :::
+                ML_Statistics.mem_print(session.head.maximum_heap).map(s =>
+                  HTML.text("heap maximum:") -> HTML.text(s)).toList :::
+                ML_Statistics.mem_print(session.head.average_heap).map(s =>
+                  HTML.text("heap average:") -> HTML.text(s)).toList :::
+                ML_Statistics.mem_print(session.head.stored_heap).map(s =>
+                  HTML.text("heap stored:") -> HTML.text(s)).toList :::
                 proper_string(session.head.isabelle_version).map(s =>
                   HTML.text("Isabelle version:") -> HTML.text(s)).toList :::
                 proper_string(session.head.afp_version).map(s =>

--- a/src/Pure/ML/ml_process.scala	Sat Feb 23 19:50:21 2019 +0000
+++ b/src/Pure/ML/ml_process.scala	Sat Feb 23 21:51:40 2019 +0100
@@ -52,19 +52,6 @@
           fun subparagraph (_: string) = ();
           val ML_file = PolyML.use;
           """,
-          if (Isabelle_System.getenv("ML_SYSTEM") == "polyml-5.6")
-            """
-              structure FixedInt = IntInf;
-              structure RunCall =
-              struct
-                open RunCall
-                val loadWord: word * word -> word =
-                  run_call2 RuntimeCalls.POLY_SYS_load_word;
-                val storeWord: word * word * word -> unit =
-                  run_call3 RuntimeCalls.POLY_SYS_assign_word;
-              end;
-            """
-          else "",
           if (Platform.is_windows)
             "fun exit 0 = OS.Process.exit OS.Process.success" +
             " | exit 1 = OS.Process.exit OS.Process.failure" +

--- a/src/Pure/ML/ml_statistics.scala	Sat Feb 23 19:50:21 2019 +0000
+++ b/src/Pure/ML/ml_statistics.scala	Sat Feb 23 21:51:40 2019 +0100
@@ -25,13 +25,22 @@
   def now(props: Properties.T): Double = Now.unapply(props).get
 
 
-  /* heap */
+  /* memory fields (mega bytes) */
+
+  def mem_print(x: Long): Option[String] =
+    if (x == 0L) None else Some(x.toString + " M")
+
+  def mem_scale(x: Long): Long = x / 1024 / 1024
 
+  def mem_field_scale(name: String, x: Double): Double =
+    if (heap_fields._2.contains(name) || program_fields._2.contains(name))
+      mem_scale(x.toLong).toDouble
+    else x
+
+  val CODE_SIZE = "size_code"
+  val STACK_SIZE = "size_stacks"
   val HEAP_SIZE = "size_heap"
 
-  def heap_scale(x: Long): Long = x / 1024 / 1024
-  def heap_scale(x: Double): Double = heap_scale(x.toLong).toLong
-
 
   /* standard fields */
 
@@ -134,7 +143,7 @@
               (x, y) <- props.iterator ++ speeds.iterator
               if x != Now.name && domain(x)
               z = java.lang.Double.parseDouble(y) if z != 0.0
-            } yield { (x.intern, if (heap_fields._2.contains(x)) heap_scale(z) else z) })
+            } yield { (x.intern, mem_field_scale(x, z)) })
 
         result += ML_Statistics.Entry(time, data)
       }
@@ -173,19 +182,14 @@
     }
   }
 
-  def maximum_heap_size: Long = maximum(ML_Statistics.HEAP_SIZE).toLong
-  def average_heap_size: Long = average(ML_Statistics.HEAP_SIZE).toLong
-
 
   /* charts */
 
   def update_data(data: XYSeriesCollection, selected_fields: List[String])
   {
     data.removeAllSeries
-    for {
-      field <- selected_fields.iterator
-      series = new XYSeries(field)
-    } {
+    for (field <- selected_fields) {
+      val series = new XYSeries(field)
       content.foreach(entry => series.add(entry.time, entry.get(field)))
       data.addSeries(series)
     }