# HG changeset patch
# User wenzelm
# Date 1476889424 -7200
# Node ID 3d5e7719e878e6eb70b9e4f6c3cc93ec0437c6a3
# Parent  3584841f2d2cb523d7e64aeed0be31e8bd9c3dd3
proper isabelle tool in Scala;

diff -r 3584841f2d2c -r 3d5e7719e878 Admin/profiling_report
--- a/Admin/profiling_report	Wed Oct 19 16:30:24 2016 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,32 +0,0 @@
-#!/usr/bin/env perl
-#
-# Author: Makarius
-#
-# DESCRIPTION: Simple report generator for Poly/ML profiling output.
-
-use strict;
-
-my %log = ();
-my @output = ();
-
-while (<ARGV>) {
-    if (m,^([ 0-9]{10}) (\S+$|GARBAGE COLLECTION.*$),) {
-	my $count = $1;
-	my $fun = $2;
-	$fun =~ s,-?\(\d+\).*$,,g;
-	$fun =~ s,/\d+$,,g;
-	if ($count =~ m,^\s*(\d)+$,) {
-	    if (defined($log{$fun})) {
-		$log{$fun} += $count;
-	    } else {
-		$log{$fun} = $count;
-	    }
-	}
-    }
-}
-
-foreach my $fun (keys %log) {
-    push @output, (sprintf "%14u %s\n", $log{$fun}, $fun);
-}
-
-print (sort @output);
diff -r 3584841f2d2c -r 3d5e7719e878 Admin/profiling_reports
--- a/Admin/profiling_reports	Wed Oct 19 16:30:24 2016 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,19 +0,0 @@
-#!/usr/bin/env bash
-#
-# Author: Makarius
-#
-# DESCRIPTION: Cumulative reports for Poly/ML profiling output.
-
-THIS="$(cd $(dirname "$0"); pwd)"
-
-SRC="$1"
-DST="$2"
-
-mkdir -p "$DST"
-
-for FILE in "$SRC"/*.gz
-do
-  echo "$FILE"
-  NAME="$(basename "$FILE" .gz)"
-  gzip -dc "$FILE" | "$THIS/profiling_report" > "$DST/$NAME"
-done
diff -r 3584841f2d2c -r 3d5e7719e878 src/Pure/Admin/profiling_report.scala
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Admin/profiling_report.scala	Wed Oct 19 17:03:44 2016 +0200
@@ -0,0 +1,55 @@
+/*  Title:      Pure/Admin/profiling_report.scala
+    Author:     Makarius
+
+Report Poly/ML profiling information from log files.
+*/
+
+package isabelle
+
+
+import java.util.Locale
+
+
+object Profiling_Report
+{
+  def profiling_report(log_file: Build_Log.Log_File): List[(Long, String)] =
+  {
+    val Line = """^(?:### )?([ 0-9]{10}) (\S+|GARBAGE COLLECTION.*)$""".r
+    val Count = """ *(\d+)""".r
+    val clean = """-?\(\d+\).*$""".r
+
+    var results = Map.empty[String, Long]
+    for (Line(Count(Value.Long(count)), raw_fun) <- log_file.lines) {
+      val fun = clean.replaceAllIn(raw_fun, "")
+      results += (fun -> (results.getOrElse(fun, 0L) + count))
+    }
+    for ((fun, count) <- results.toList.sortBy(_._2)) yield (count, fun)
+  }
+
+
+  /* Isabelle tool wrapper */
+
+  val isabelle_tool =
+    Isabelle_Tool("profiling_report", "report Poly/ML profiling information from log files", args =>
+    {
+      Command_Line.tool0 {
+        val getopts =
+          Getopts("""
+Usage: isabelle profiling_report [LOGS ...]
+
+  Report Poly/ML profiling output from log files (potentially compressed).
+""")
+        val log_names = getopts(args)
+        for (name <- log_names) {
+          val log_file = Build_Log.Log_File(Path.explode(name))
+          val results =
+            for ((count, fun) <- profiling_report(log_file))
+              yield
+                String.format(Locale.ROOT, "%14d %s",
+                  count.asInstanceOf[AnyRef], fun.asInstanceOf[AnyRef])
+          if (results.nonEmpty)
+            Output.writeln(cat_lines((log_file.name + ":") :: results))
+        }
+      }
+    })
+}
diff -r 3584841f2d2c -r 3d5e7719e878 src/Pure/System/isabelle_tool.scala
--- a/src/Pure/System/isabelle_tool.scala	Wed Oct 19 16:30:24 2016 +0200
+++ b/src/Pure/System/isabelle_tool.scala	Wed Oct 19 17:03:44 2016 +0200
@@ -106,6 +106,7 @@
       Doc.isabelle_tool,
       ML_Process.isabelle_tool,
       Options.isabelle_tool,
+      Profiling_Report.isabelle_tool,
       Remote_DMG.isabelle_tool,
       Update_Cartouches.isabelle_tool,
       Update_Header.isabelle_tool,
diff -r 3584841f2d2c -r 3d5e7719e878 src/Pure/build-jars
--- a/src/Pure/build-jars	Wed Oct 19 16:30:24 2016 +0200
+++ b/src/Pure/build-jars	Wed Oct 19 17:03:44 2016 +0200
@@ -19,6 +19,7 @@
   Admin/ci_profile.scala
   Admin/isabelle_cronjob.scala
   Admin/other_isabelle.scala
+  Admin/profiling_report.scala
   Admin/remote_dmg.scala
   Concurrent/consumer_thread.scala
   Concurrent/counter.scala