src/Pure/ML/ml_heap.scala
changeset 79706 4f218e6e9d23
parent 79698 b676998d7f97
child 79719 8544f1045123
equal deleted inserted replaced
79705:a6dc0d4ffea2 79706:4f218e6e9d23
    86         body = "SELECT name, slice, pg_size_pretty(length(content)::bigint) as size FROM " +
    86         body = "SELECT name, slice, pg_size_pretty(length(content)::bigint) as size FROM " +
    87           Slices.table.ident,
    87           Slices.table.ident,
    88         name = "slices_size")
    88         name = "slices_size")
    89     }
    89     }
    90 
    90 
    91     def read_digests(db: SQL.Database, names: Iterable[String]): Map[String, SHA1.Digest] = {
    91     def read_digests(db: SQL.Database, names: Iterable[String]): Map[String, SHA1.Digest] =
    92       db.execute_query_statement(
    92       if (names.isEmpty) Map.empty
    93         Base.table.select(List(Base.name, Base.heap_digest),
    93       else {
    94           sql = Generic.name.where_member(names)),
    94         db.execute_query_statement(
    95         List.from[(String, String)],
    95           Base.table.select(List(Base.name, Base.heap_digest),
    96         res => res.string(Base.name) -> res.string(Base.heap_digest)
    96             sql = Generic.name.where_member(names)),
    97       ).collect({
    97           List.from[(String, String)],
    98         case (name, digest) if digest.nonEmpty => name -> SHA1.fake_digest(digest)
    98           res => res.string(Base.name) -> res.string(Base.heap_digest)
    99       }).toMap
    99         ).collect({
   100     }
   100           case (name, digest) if digest.nonEmpty => name -> SHA1.fake_digest(digest)
       
   101         }).toMap
       
   102       }
   101 
   103 
   102     def read_slices(db: SQL.Database, name: String): List[Bytes] =
   104     def read_slices(db: SQL.Database, name: String): List[Bytes] =
   103       db.execute_query_statement(
   105       db.execute_query_statement(
   104         Slices.table.select(List(Slices.content),
   106         Slices.table.select(List(Slices.content),
   105           sql = Generic.name.where_equal(name) + SQL.order_by(List(Slices.slice))),
   107           sql = Generic.name.where_equal(name) + SQL.order_by(List(Slices.slice))),