src/Pure/Admin/build_stats.scala
changeset 65742 b9e0f25ba16a
parent 65741 cf42659364c9
equal deleted inserted replaced
65741:cf42659364c9 65742:b9e0f25ba16a
    61 
    61 
    62     val store = Build_Log.store(options)
    62     val store = Build_Log.store(options)
    63     using(store.open_database())(db =>
    63     using(store.open_database())(db =>
    64     {
    64     {
    65       for (profile <- profiles) {
    65       for (profile <- profiles) {
    66         progress.echo("database query " + quote(profile.name))
    66         progress.echo("input " + quote(profile.name))
    67         val columns =
    67         val columns =
    68           List(
    68           List(
    69             Build_Log.Data.pull_date,
    69             Build_Log.Data.pull_date,
    70             Build_Log.Settings.ML_PLATFORM,
    70             Build_Log.Settings.ML_PLATFORM,
    71             Build_Log.Data.session_name,
    71             Build_Log.Data.session_name,
   143     ml_timing: Option[Boolean] = None)
   143     ml_timing: Option[Boolean] = None)
   144   {
   144   {
   145     val data_entries = data.toList.sortBy(_._1)
   145     val data_entries = data.toList.sortBy(_._1)
   146     for ((name, session_entries) <- data_entries) {
   146     for ((name, session_entries) <- data_entries) {
   147       val dir = target_dir + Path.explode(name)
   147       val dir = target_dir + Path.explode(name)
   148       progress.echo("directory " + dir)
   148       progress.echo("output " + dir)
   149       Isabelle_System.mkdirs(dir)
   149       Isabelle_System.mkdirs(dir)
   150 
   150 
   151       for ((session, entries) <- session_entries) {
   151       for ((session, entries) <- session_entries) {
   152         Isabelle_System.with_tmp_file(session, "data") { data_file =>
   152         Isabelle_System.with_tmp_file(session, "data") { data_file =>
   153           Isabelle_System.with_tmp_file(session, "gnuplot") { gnuplot_file =>
   153           Isabelle_System.with_tmp_file(session, "gnuplot") { gnuplot_file =>
   194 plot [] [0:] """ + plots.map(s => quote(data_file.implode) + " " + s).mkString(", ") + "\n")
   194 plot [] [0:] """ + plots.map(s => quote(data_file.implode) + " " + s).mkString(", ") + "\n")
   195 
   195 
   196             val result =
   196             val result =
   197               Isabelle_System.bash("\"$ISABELLE_GNUPLOT\" " + File.bash_path(gnuplot_file))
   197               Isabelle_System.bash("\"$ISABELLE_GNUPLOT\" " + File.bash_path(gnuplot_file))
   198             if (result.rc != 0)
   198             if (result.rc != 0)
   199               result.error("Gnuplot error in " + name + "/" + session).check
   199               result.error("Gnuplot failed for " + name + "/" + session).check
   200           }
   200           }
   201         }
   201         }
   202       }
   202       }
   203 
   203 
   204       File.write(dir + Path.basic("index.html"),
   204       File.write(dir + Path.basic("index.html"),