operations to read database;

--- a/src/Pure/Admin/build_log.scala	Fri Apr 28 21:33:31 2017 +0200
+++ b/src/Pure/Admin/build_log.scala	Fri Apr 28 22:29:37 2017 +0200
@@ -28,9 +28,12 @@
   {
     val separator = '\u000b'
 
+    def cat_multiple(args: List[String]): String =
+      args.mkString(separator.toString)
+
     def multiple(name: String, args: List[String]): Properties.T =
       if (args.isEmpty) Nil
-      else List(name -> args.mkString(separator.toString))
+      else List(name -> cat_multiple(args))
 
     def multiple_lines(s: String): String =
       cat_lines(Library.space_explode(separator, s))
@@ -688,6 +691,28 @@
       }
     }
 
+    def read_meta_info(db: SQL.Database, log_name: String): Option[Meta_Info] =
+    {
+      val cs = Meta_Info.table.columns.tail
+      using(db.select(Meta_Info.table, cs, Meta_Info.log_name.sql_where_equal(log_name)))(stmt =>
+      {
+        val rs = stmt.executeQuery
+        if (!rs.next) None
+        else {
+          val results =
+            cs.map(c => c.name ->
+              (if (c.T == SQL.Type.Date)
+                db.get(rs, c, db.date _).map(Log_File.Date_Format(_))
+               else
+                db.get(rs, c, db.string _).map(s => Prop.cat_multiple(split_lines(s)))))
+          val n = Prop.all_props.length
+          val props = for ((x, Some(y)) <- results.take(n)) yield (x, y)
+          val settings = for ((x, Some(y)) <- results.drop(n)) yield (x, y)
+          Some(Meta_Info(props, settings))
+        }
+      })
+    }
+
     def write_build_info(db: SQL.Database, files: List[JFile])
     {
       for (file_group <- filter_files(db, Build_Info.table, files).grouped(100)) {
@@ -722,5 +747,43 @@
         }
       }
     }
+
+    def read_build_info(
+      db: SQL.Database, log_name: String, session_names: List[String] = Nil): Build_Info =
+    {
+      val where_log_name = Meta_Info.log_name.sql_where_equal(log_name)
+      val where =
+        if (session_names.isEmpty) where_log_name
+        else
+          where_log_name + " AND " +
+          session_names.map(a => Build_Info.session_name.sql_name + " = " + SQL.quote_string(a)).
+            mkString("(", " OR ", ")")
+      val sessions =
+        using(db.select(Build_Info.table, Build_Info.table.columns.tail, where))(stmt =>
+        {
+          SQL.iterator(stmt.executeQuery)(rs =>
+          {
+            val session_name = db.string(rs, Build_Info.session_name)
+            val chapter = db.string(rs, Build_Info.chapter)
+            val groups = split_lines(db.string(rs, Build_Info.groups))
+            val threads = db.get(rs, Build_Info.threads, db.int _)
+            val timing_elapsed = Time.ms(db.long(rs, Build_Info.timing_elapsed))
+            val timing_cpu = Time.ms(db.long(rs, Build_Info.timing_cpu))
+            val timing_gc = Time.ms(db.long(rs, Build_Info.timing_gc))
+            val ml_timing_elapsed = Time.ms(db.long(rs, Build_Info.ml_timing_elapsed))
+            val ml_timing_cpu = Time.ms(db.long(rs, Build_Info.ml_timing_cpu))
+            val ml_timing_gc = Time.ms(db.long(rs, Build_Info.ml_timing_gc))
+            val ml_statistics = uncompress_properties(db.bytes(rs, Build_Info.ml_statistics))
+            val heap_size = db.get(rs, Build_Info.heap_size, db.long _)
+            val status = Session_Status.withName(db.string(rs, Build_Info.status))
+
+            session_name ->
+              Session_Entry(chapter, groups, threads, Timing(timing_elapsed, timing_cpu, timing_gc),
+                Timing(ml_timing_elapsed, ml_timing_cpu, ml_timing_gc), ml_statistics,
+                heap_size, status)
+          }).toMap
+        })
+      Build_Info(sessions)
+    }
   }
 }