more SQL operations;

--- a/src/Pure/Admin/build_history.scala	Wed Apr 26 16:30:11 2017 +0200
+++ b/src/Pure/Admin/build_history.scala	Thu Apr 27 11:19:22 2017 +0200
@@ -211,16 +211,16 @@
       val store = Sessions.store()
 
       val meta_info =
-        Build_Log.Prop.multiple(Build_Log.Prop.build_tags, build_tags) :::
-        Build_Log.Prop.multiple(Build_Log.Prop.build_args, build_args1) :::
+        Build_Log.Prop.multiple(Build_Log.Prop.build_tags.name, build_tags) :::
+        Build_Log.Prop.multiple(Build_Log.Prop.build_args.name, build_args1) :::
         List(
-          Build_Log.Prop.build_group_id -> build_group_id,
-          Build_Log.Prop.build_id -> (build_host + ":" + build_start.time.ms),
-          Build_Log.Prop.build_engine -> Build_History.engine,
-          Build_Log.Prop.build_host -> build_host,
-          Build_Log.Prop.build_start -> Build_Log.print_date(build_start),
-          Build_Log.Prop.build_end -> Build_Log.print_date(build_end),
-          Build_Log.Prop.isabelle_version -> isabelle_version)
+          Build_Log.Prop.build_group_id.name -> build_group_id,
+          Build_Log.Prop.build_id.name -> (build_host + ":" + build_start.time.ms),
+          Build_Log.Prop.build_engine.name -> Build_History.engine,
+          Build_Log.Prop.build_host.name -> build_host,
+          Build_Log.Prop.build_start.name -> Build_Log.print_date(build_start),
+          Build_Log.Prop.build_end.name -> Build_Log.print_date(build_end),
+          Build_Log.Prop.isabelle_version.name -> isabelle_version)
 
       val ml_statistics =
         build_info.finished_sessions.flatMap(session_name =>

--- a/src/Pure/Admin/build_log.scala	Wed Apr 26 16:30:11 2017 +0200
+++ b/src/Pure/Admin/build_log.scala	Thu Apr 27 11:19:22 2017 +0200
@@ -30,16 +30,20 @@
       if (args.isEmpty) Nil
       else List(name -> args.mkString(separator.toString))
 
-    val build_tags = "build_tags"  // multiple
-    val build_args = "build_args"  // multiple
-    val build_group_id = "build_group_id"
-    val build_id = "build_id"
-    val build_engine = "build_engine"
-    val build_host = "build_host"
-    val build_start = "build_start"
-    val build_end = "build_end"
-    val isabelle_version = "isabelle_version"
-    val afp_version = "afp_version"
+    val build_tags = SQL.Column.string("build_tags")  // multiple
+    val build_args = SQL.Column.string("build_args")  // multiple
+    val build_group_id = SQL.Column.string("build_group_id")
+    val build_id = SQL.Column.string("build_id")
+    val build_engine = SQL.Column.string("build_engine")
+    val build_host = SQL.Column.string("build_host")
+    val build_start = SQL.Column.date("build_start")
+    val build_end = SQL.Column.date("build_end")
+    val isabelle_version = SQL.Column.string("isabelle_version")
+    val afp_version = SQL.Column.string("afp_version")
+
+    val columns: List[SQL.Column] =
+      List(build_tags, build_args, build_group_id, build_id, build_engine,
+        build_host, build_start, build_end, isabelle_version, afp_version)
   }
 
 
@@ -273,6 +277,11 @@
   object Meta_Info
   {
     val empty: Meta_Info = Meta_Info(Nil, Nil)
+
+    val log_filename = SQL.Column.string("log_filename", primary_key = true)
+
+    val columns: List[SQL.Column] =
+      log_filename :: Prop.columns ::: Settings.all_settings.map(SQL.Column.string(_))
   }
 
   sealed case class Meta_Info(props: Properties.T, settings: List[(String, String)])
@@ -325,23 +334,23 @@
         val prefix = if (host != "") host else if (engine != "") engine else ""
         (if (prefix == "") "build" else prefix) + ":" + start.time.ms
       }
-      val build_engine = if (engine == "") Nil else List(Prop.build_engine -> engine)
-      val build_host = if (host == "") Nil else List(Prop.build_host -> host)
+      val build_engine = if (engine == "") Nil else List(Prop.build_engine.name -> engine)
+      val build_host = if (host == "") Nil else List(Prop.build_host.name -> host)
 
-      val start_date = List(Prop.build_start -> start.toString)
+      val start_date = List(Prop.build_start.name -> start.toString)
       val end_date =
         log_file.lines.last match {
           case End(log_file.Strict_Date(end_date)) =>
-            List(Prop.build_end -> end_date.toString)
+            List(Prop.build_end.name -> end_date.toString)
           case _ => Nil
         }
 
       val isabelle_version =
-        log_file.find_match(Isabelle_Version).map(Prop.isabelle_version -> _)
+        log_file.find_match(Isabelle_Version).map(Prop.isabelle_version.name -> _)
       val afp_version =
-        log_file.find_match(AFP_Version).map(Prop.afp_version -> _)
+        log_file.find_match(AFP_Version).map(Prop.afp_version.name -> _)
 
-      Meta_Info((Prop.build_id -> build_id) :: build_engine ::: build_host :::
+      Meta_Info((Prop.build_id.name -> build_id) :: build_engine ::: build_host :::
           start_date ::: end_date ::: isabelle_version.toList ::: afp_version.toList,
         log_file.get_settings(Settings.all_settings))
     }