# HG changeset patch
# User wenzelm
# Date 1476784238 -7200
# Node ID 12a47f263122ea8d8a0f4a73342a35facb7f0c5d
# Parent  544481988e659ea322a2289bbce6f63fea70ff1c
support for free-form build tags;
tuned;

diff -r 544481988e65 -r 12a47f263122 src/Pure/Admin/build_history.scala
--- a/src/Pure/Admin/build_history.scala	Tue Oct 18 11:24:14 2016 +0200
+++ b/src/Pure/Admin/build_history.scala	Tue Oct 18 11:50:38 2016 +0200
@@ -115,6 +115,7 @@
     max_heap: Option[Int] = None,
     more_settings: List[String] = Nil,
     verbose: Boolean = false,
+    build_tags: List[String] = Nil,
     build_args: List[String] = Nil): List[(Process_Result, Path)] =
   {
     /* sanity checks */
@@ -191,8 +192,8 @@
       val log_path =
         other_isabelle.isabelle_home_user +
           Build_Log.log_subdir(build_history_date) +
-          Build_Log.log_filename(
-            BUILD_HISTORY, build_history_date, build_host, ml_platform, "M" + threads)
+          Build_Log.log_filename(BUILD_HISTORY, build_history_date,
+            List(build_host, ml_platform, "M" + threads) ::: build_tags)
 
       val build_info =
         Build_Log.Log_File(log_path.base.implode, build_result.out_lines).parse_build_info()
@@ -201,6 +202,8 @@
       /* output log */
 
       val meta_info =
+        (if (build_tags.isEmpty) Nil
+         else List(Build_Log.Field.build_tags -> Word.implode(build_tags))) :::
         List(
           Build_Log.Field.build_group_id -> build_group_id,
           Build_Log.Field.build_id -> (build_host + ":" + build_start.time.ms),
@@ -268,6 +271,7 @@
       var arch_64 = false
       var nonfree = false
       var rev = default_rev
+      var build_tags = List.empty[String]
       var verbose = false
 
       val getopts = Getopts("""
@@ -285,6 +289,7 @@
     -m ARCH      processor architecture (32=x86, 64=x86_64, default: x86)
     -n           include nonfree components
     -r REV       update to revision (default: """ + default_rev + """)
+    -t TAG       free-form build tag (multiple occurrences possible)
     -v           verbose
 
   Build Isabelle sessions from the history of another REPOSITORY clone,
@@ -306,6 +311,7 @@
           },
         "n" -> (_ => nonfree = true),
         "r:" -> (arg => rev = arg),
+        "t:" -> (arg => build_tags = build_tags ::: List(arg)),
         "v" -> (_ => verbose = true))
 
       val more_args = getopts(args)
@@ -323,7 +329,7 @@
           multicore_base = multicore_base, threads_list = threads_list, arch_64 = arch_64,
           heap = heap.getOrElse(if (arch_64) default_heap * 2 else default_heap),
           max_heap = max_heap, more_settings = more_settings, verbose = verbose,
-          build_args = build_args)
+          build_tags = build_tags, build_args = build_args)
 
       for ((_, log_path) <- results)
         Output.writeln(log_path.implode, stdout = true)
diff -r 544481988e65 -r 12a47f263122 src/Pure/Admin/build_log.scala
--- a/src/Pure/Admin/build_log.scala	Tue Oct 18 11:24:14 2016 +0200
+++ b/src/Pure/Admin/build_log.scala	Tue Oct 18 11:50:38 2016 +0200
@@ -30,8 +30,8 @@
   def log_subdir(date: Date): Path =
     Path.explode("log") + Path.explode(date.rep.getYear.toString)
 
-  def log_filename(engine: String, date: Date, more: String*): Path =
-    Path.explode((engine :: log_date(date) :: more.toList).mkString("", "_", ".log"))
+  def log_filename(engine: String, date: Date, more: List[String] = Nil): Path =
+    Path.explode((engine :: log_date(date) :: more).mkString("", "_", ".log"))
 
 
   /* log file collections */
@@ -247,6 +247,7 @@
 
   object Field
   {
+    val build_tags = "build_tags"
     val build_group_id = "build_group_id"
     val build_id = "build_id"
     val build_engine = "build_engine"