--- a/src/Pure/Thy/document_build.scala Fri Feb 24 20:52:35 2023 +0100
+++ b/src/Pure/Thy/document_build.scala Sat Feb 25 14:33:19 2023 +0100
@@ -64,8 +64,10 @@
val table = SQL.Table("isabelle_documents", List(session_name, name, sources, log_xz, pdf))
def where_equal(session_name: String, name: String = ""): SQL.Source =
- "WHERE " + Data.session_name.equal(session_name) +
- (if (name == "") "" else " AND " + Data.name.equal(name))
+ SQL.where(
+ SQL.and(
+ Data.session_name.equal(session_name),
+ if_proper(name, Data.name.equal(name))))
}
def read_documents(db: SQL.Database, session_name: String): List[Document_Input] = {