--- a/src/Pure/Thy/sessions.scala Sat Jun 20 15:09:20 2020 +0200
+++ b/src/Pure/Thy/sessions.scala Sat Jun 20 16:18:33 2020 +0200
@@ -1085,6 +1085,9 @@
{
override def toString: String = "Store(output_dir = " + output_dir.expand + ")"
+ val xml_cache: XML.Cache = XML.make_cache()
+ val xz_cache: XZ.Cache = XZ.make_cache()
+
/* directories */
@@ -1199,9 +1202,6 @@
/* SQL database content */
- 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),
Session_Info.session_name.where_equal(name)))(stmt =>