changeset 68294 | 0f513ae3db77 |
parent 68292 | 7ca0c23179e6 |
child 68304 | 09270aa40884 |
--- a/src/Pure/Thy/sessions.scala Sat May 26 21:23:51 2018 +0200 +++ b/src/Pure/Thy/sessions.scala Sat May 26 21:24:07 2018 +0200 @@ -1092,8 +1092,8 @@ /* SQL database content */ - val xml_cache = XML.make_cache() - val xz_cache = XZ.make_cache() + val xml_cache: XML.Cache = XML.make_cache() + val xz_cache: XZ.Cache = XZ.make_cache() def read_bytes(db: SQL.Database, name: String, column: SQL.Column): Bytes = db.using_statement(Session_Info.table.select(List(column),