src/Pure/ML/ml_heap.scala
changeset 79689 fabe9f89911f
parent 79688 3abfc5ebabad
child 79690 ecc851dd274f
equal deleted inserted replaced
79688:3abfc5ebabad 79689:fabe9f89911f
    92           Slices.table.ident,
    92           Slices.table.ident,
    93         name = "slices_size")
    93         name = "slices_size")
    94     }
    94     }
    95 
    95 
    96     def read_digests(db: SQL.Database, names: Iterable[String]): Map[String, SHA1.Digest] = {
    96     def read_digests(db: SQL.Database, names: Iterable[String]): Map[String, SHA1.Digest] = {
    97       require(names.nonEmpty)
       
    98 
       
    99       db.execute_query_statement(
    97       db.execute_query_statement(
   100         Base.table.select(List(Base.name, Base.heap_digest),
    98         Base.table.select(List(Base.name, Base.heap_digest),
   101           sql = Generic.name.where_member(names)),
    99           sql = Generic.name.where_member(names)),
   102         List.from[(String, String)],
   100         List.from[(String, String)],
   103         res => res.string(Base.name) -> res.string(Base.heap_digest)
   101         res => res.string(Base.name) -> res.string(Base.heap_digest)
   104       ).flatMap({
   102       ).collect({
   105         case (_, "") => None
   103         case (name, digest) if digest.nonEmpty => name -> SHA1.fake_digest(digest)
   106         case (name, digest) => Some(name -> SHA1.fake_digest(digest))
       
   107       }).toMap
   104       }).toMap
   108     }
   105     }
   109 
   106 
   110     def read_slices(db: SQL.Database, name: String): List[Bytes] =
   107     def read_slices(db: SQL.Database, name: String): List[Bytes] =
   111       db.execute_query_statement(
   108       db.execute_query_statement(