src/Pure/Admin/build_log.scala
changeset 65688 2181b5615c64
parent 65685 47bbf7150aae
child 65689 c1eab527bfa7
equal deleted inserted replaced
65686:4a762cad298f 65688:2181b5615c64
   684         ssh =
   684         ssh =
   685           if (ssh_host == "") None
   685           if (ssh_host == "") None
   686           else Some(SSH.init_context(options).open_session(ssh_host, ssh_user, port)),
   686           else Some(SSH.init_context(options).open_session(ssh_host, ssh_user, port)),
   687         ssh_close = true)
   687         ssh_close = true)
   688     }
   688     }
       
   689 
       
   690     def domain(db: SQL.Database, table: SQL.Table, column: SQL.Column): Set[String] =
       
   691       using(db.select(table, List(column), distinct = true))(stmt =>
       
   692         SQL.iterator(stmt.executeQuery)(db.string(_, column)).toSet)
   689 
   693 
   690     def update_meta_info(db: SQL.Database, log_file: Log_File)
   694     def update_meta_info(db: SQL.Database, log_file: Log_File)
   691     {
   695     {
   692       val meta_info = log_file.parse_meta_info()
   696       val meta_info = log_file.parse_meta_info()
   693       val table = Meta_Info.table
   697       val table = Meta_Info.table
   768 
   772 
   769     def write_info(db: SQL.Database, files: List[JFile], ml_statistics: Boolean = false)
   773     def write_info(db: SQL.Database, files: List[JFile], ml_statistics: Boolean = false)
   770     {
   774     {
   771       class Table_Status(table: SQL.Table, update_db: (SQL.Database, Log_File) => Unit)
   775       class Table_Status(table: SQL.Table, update_db: (SQL.Database, Log_File) => Unit)
   772       {
   776       {
   773         private var known: Set[String] =
   777         db.create_table(table)
   774         {
   778         private var known: Set[String] = domain(db, table, Meta_Info.log_name)
   775           db.create_table(table)
   779 
   776           val key = Meta_Info.log_name
       
   777           using(db.select(table, List(key), distinct = true))(
       
   778             stmt => SQL.iterator(stmt.executeQuery)(db.string(_, key)).toSet)
       
   779         }
       
   780         def required(file: JFile): Boolean = !known(Log_File.plain_name(file.getName))
   780         def required(file: JFile): Boolean = !known(Log_File.plain_name(file.getName))
   781         def update(log_file: Log_File)
   781         def update(log_file: Log_File)
   782         {
   782         {
   783           if (!known(log_file.name)) {
   783           if (!known(log_file.name)) {
   784             update_db(db, log_file)
   784             update_db(db, log_file)