# HG changeset patch
# User wenzelm
# Date 1688731733 -7200
# Node ID 316afcb8dc0cd7b9eea60e37fcb07f9b062fb96d
# Parent  0a7f7abbe4f08d1351ab7f3763e0cbcbfda0c584
unused (see also ea35afdb1366);

diff -r 0a7f7abbe4f0 -r 316afcb8dc0c src/Pure/Thy/document_build.scala
--- a/src/Pure/Thy/document_build.scala	Fri Jul 07 14:04:52 2023 +0200
+++ b/src/Pure/Thy/document_build.scala	Fri Jul 07 14:08:53 2023 +0200
@@ -75,17 +75,6 @@
     def clean_session(db: SQL.Database, session_name: String): Unit =
       db.execute_statement(Base.table.delete(sql = Base.session_name.where_equal(session_name)))
 
-    def read_documents(db: SQL.Database, session_name: String): List[Document_Input] =
-      db.execute_query_statement(
-        Base.table.select(List(Base.name, Base.sources), sql = where_equal(session_name)),
-        List.from[Document_Input],
-        { res =>
-          val name = res.string(Base.name)
-          val sources = res.string(Base.sources)
-          Document_Input(name, SHA1.fake_shasum(sources))
-        }
-      )
-
     def read_document(
       db: SQL.Database,
       session_name: String,
@@ -117,9 +106,6 @@
   def clean_session(db: SQL.Database, session_name: String): Unit =
     Data.transaction_lock(db, create = true) { Data.clean_session(db, session_name) }
 
-  def read_documents(db: SQL.Database, session_name: String): List[Document_Input] =
-    Data.transaction_lock(db) { Data.read_documents(db, session_name) }
-
   def read_document(db: SQL.Database, session_name: String, name: String): Option[Document_Output] =
     Data.transaction_lock(db) { Data.read_document(db, session_name, name) }