--- a/src/Pure/Thy/sessions.scala Fri Feb 24 20:52:35 2023 +0100
+++ b/src/Pure/Thy/sessions.scala Sat Feb 25 14:33:19 2023 +0100
@@ -77,8 +77,10 @@
SQL.Table("isabelle_sources", List(session_name, name, digest, compressed, body))
def where_equal(session_name: String, name: String = ""): SQL.Source =
- "WHERE " + Sources.session_name.equal(session_name) +
- (if (name == "") "" else " AND " + Sources.name.equal(name))
+ SQL.where(
+ SQL.and(
+ Sources.session_name.equal(session_name),
+ if_proper(name, Sources.name.equal(name))))
def load(session_base: Base, cache: Compress.Cache = Compress.Cache.none): Sources =
new Sources(