# HG changeset patch
# User wenzelm
# Date 1494352951 -7200
# Node ID cf48ef4f4e6343cc4c4a76b773c16e685e72acec
# Parent  91940684a2676b850548b7737df94486fcee8671
tuned;

diff -r 91940684a267 -r cf48ef4f4e63 src/Pure/Admin/build_status.scala
--- a/src/Pure/Admin/build_status.scala	Tue May 09 19:57:04 2017 +0200
+++ b/src/Pure/Admin/build_status.scala	Tue May 09 20:02:31 2017 +0200
@@ -9,6 +9,28 @@
 
 object Build_Status
 {
+  /* data profiles */
+
+  sealed case class Profile(description: String, sql: String)
+  {
+    def select(columns: List[SQL.Column], days: Int, only_sessions: Set[String]): SQL.Source =
+    {
+      val sql_sessions =
+        if (only_sessions.isEmpty) ""
+        else
+          only_sessions.iterator.map(a => Build_Log.Data.session_name + " = " + SQL.string(a))
+            .mkString("(", " OR ", ") AND ")
+
+      Build_Log.Data.universal_table.select(columns, distinct = true,
+        sql = "WHERE " +
+          Build_Log.Data.pull_date + " > " + Build_Log.Data.recent_time(days) + " AND " +
+          Build_Log.Data.status + " = " + SQL.string(Build_Log.Session_Status.finished.toString) +
+          " AND " + sql_sessions + SQL.enclose(sql) +
+          " ORDER BY " + Build_Log.Data.pull_date + " DESC")
+    }
+  }
+
+
   /* build status */
 
   val default_target_dir = Path.explode("build_status")
@@ -33,30 +55,7 @@
   }
 
 
-  /* data profiles */
-
-  def clean_name(name: String): String =
-    name.flatMap(c => if (c == ' ' || c == '/') "_" else if (c == ',') "" else c.toString)
-
-  sealed case class Profile(description: String, sql: String)
-  {
-    def select(columns: List[SQL.Column], days: Int, only_sessions: Set[String]): SQL.Source =
-    {
-      val sql_sessions =
-        if (only_sessions.isEmpty) ""
-        else
-          only_sessions.iterator.map(a => Build_Log.Data.session_name + " = " + SQL.string(a))
-            .mkString("(", " OR ", ") AND ")
-
-      Build_Log.Data.universal_table.select(columns, distinct = true,
-        sql = "WHERE " +
-          Build_Log.Data.pull_date + " > " + Build_Log.Data.recent_time(days) + " AND " +
-          Build_Log.Data.status + " = " + SQL.string(Build_Log.Session_Status.finished.toString) +
-          " AND " + sql_sessions + SQL.enclose(sql) +
-          " ORDER BY " + Build_Log.Data.pull_date + " DESC")
-    }
-  }
-
+  /* read data */
 
   sealed case class Data(date: Date, entries: List[(String, List[Session])])
   sealed case class Session(name: String, threads: Int, entries: List[Entry])
@@ -70,9 +69,6 @@
   }
   sealed case class Entry(date: Date, timing: Timing, ml_timing: Timing, heap_size: Long)
 
-
-  /* read data */
-
   def read_data(options: Options,
     progress: Progress = No_Progress,
     profiles: List[Profile] = default_profiles,
@@ -165,6 +161,9 @@
     target_dir: Path = default_target_dir,
     image_size: (Int, Int) = default_image_size)
   {
+    def clean_name(name: String): String =
+      name.flatMap(c => if (c == ' ' || c == '/') "_" else if (c == ',') "" else c.toString)
+
     Isabelle_System.mkdirs(target_dir)
     File.write(target_dir + Path.basic("index.html"),
       HTML.output_document(