src/Pure/Admin/build_log.scala
changeset 65708 50a61990c01e
parent 65706 595bc96005f9
child 65709 1626b73daccf
equal deleted inserted replaced
65707:353b965378cf 65708:50a61990c01e
   808 
   808 
   809             // full view
   809             // full view
   810             db2.create_view(Data.full_table)
   810             db2.create_view(Data.full_table)
   811           }
   811           }
   812         }
   812         }
       
   813         db2.rebuild
   813       })
   814       })
   814     }
   815     }
   815 
   816 
   816     def domain(db: SQL.Database, table: SQL.Table, column: SQL.Column): Set[String] =
   817     def domain(db: SQL.Database, table: SQL.Table, column: SQL.Column): Set[String] =
   817       db.using_statement(table.select(List(column), distinct = true))(stmt =>
   818       db.using_statement(table.select(List(column), distinct = true))(stmt =>