# HG changeset patch
# User wenzelm
# Date 1527362647 -7200
# Node ID 0f513ae3db77c413355267f87e4fe04b553070c2
# Parent  2bc4e5d9cca6ee62a6d192671dc47787c8a2fafb
tuned;

diff -r 2bc4e5d9cca6 -r 0f513ae3db77 src/Pure/Thy/sessions.scala
--- 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),