# HG changeset patch
# User wenzelm
# Date 1659448926 -7200
# Node ID 288c4d4042cc90083a455529f34b7cd899acb5e7
# Parent  6b319113b3a4a518b68ef81ba36c762af08e6d27
clarified signature;

diff -r 6b319113b3a4 -r 288c4d4042cc src/Pure/Thy/document_build.scala
--- a/src/Pure/Thy/document_build.scala	Tue Aug 02 15:53:48 2022 +0200
+++ b/src/Pure/Thy/document_build.scala	Tue Aug 02 16:02:06 2022 +0200
@@ -253,7 +253,7 @@
 
     def old_document(directory: Directory): Option[Document_Output] =
       for {
-        old_doc <- db_context.input_database(session)(read_document(_, _, directory.doc.name))
+        old_doc <- db_context.input_database(session)(read_document(_, session, directory.doc.name))
         if old_doc.sources == directory.sources
       }
       yield old_doc
diff -r 6b319113b3a4 -r 288c4d4042cc src/Pure/Thy/presentation.scala
--- a/src/Pure/Thy/presentation.scala	Tue Aug 02 15:53:48 2022 +0200
+++ b/src/Pure/Thy/presentation.scala	Tue Aug 02 16:02:06 2022 +0200
@@ -125,7 +125,7 @@
       val theory_node_info =
         Par_List.map[Batch, List[(String, Node_Info)]](
           { case (session, thys) =>
-              db_context.input_database(session) { (db, _) =>
+              db_context.input_database(session) { db =>
                 val provider0 = Export.Provider.database(db, db_context.cache, session, "")
                 val result =
                   for (thy_name <- thys) yield {
@@ -530,7 +530,8 @@
     val documents =
       for {
         doc <- info.document_variants
-        document <- db_context.input_database(session)(Document_Build.read_document(_, _, doc.name))
+        document <- db_context.input_database(session)(db =>
+          Document_Build.read_document(db, session, doc.name))
       } yield {
         val doc_path = (session_dir + doc.path.pdf).expand
         if (verbose) progress.echo("Presenting document " + session + "/" + doc.name)
diff -r 6b319113b3a4 -r 288c4d4042cc src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Tue Aug 02 15:53:48 2022 +0200
+++ b/src/Pure/Thy/sessions.scala	Tue Aug 02 16:02:06 2022 +0200
@@ -1206,12 +1206,12 @@
         case None => using(store.open_database(session, output = true))(f)
       }
 
-    def input_database[A](session: String)(f: (SQL.Database, String) => Option[A]): Option[A] =
+    def input_database[A](session: String)(f: SQL.Database => Option[A]): Option[A] =
       database_server match {
-        case Some(db) => f(db, session)
+        case Some(db) => f(db)
         case None =>
           store.try_open_database(session) match {
-            case Some(db) => using(db)(f(_, session))
+            case Some(db) => using(db)(f)
             case None => None
           }
       }
@@ -1244,7 +1244,7 @@
         name <- structure.build_requirements(List(session))
         patterns = structure(name).export_classpath if patterns.nonEmpty
       } yield {
-        input_database(name)((db, _) =>
+        input_database(name) { db =>
           db.transaction {
             val matcher = Export.make_matcher(patterns)
             val res =
@@ -1254,7 +1254,7 @@
               } yield File.Content(entry.entry_name.make_path(), entry.uncompressed)
             Some(res)
           }
-        ).getOrElse(Nil)
+        }.getOrElse(Nil)
       }).flatten
     }
 
diff -r 6b319113b3a4 -r 288c4d4042cc src/Pure/Tools/build_job.scala
--- a/src/Pure/Tools/build_job.scala	Tue Aug 02 15:53:48 2022 +0200
+++ b/src/Pure/Tools/build_job.scala	Tue Aug 02 16:02:06 2022 +0200
@@ -94,7 +94,7 @@
 
     using(store.open_database_context()) { db_context =>
       val result =
-        db_context.input_database(session_name) { (db, _) =>
+        db_context.input_database(session_name) { db =>
           val theories = store.read_theories(db, session_name)
           val errors = store.read_errors(db, session_name)
           store.read_build(db, session_name).map(info => (theories, errors, info.return_code))
diff -r 6b319113b3a4 -r 288c4d4042cc src/Pure/Tools/profiling_report.scala
--- a/src/Pure/Tools/profiling_report.scala	Tue Aug 02 15:53:48 2022 +0200
+++ b/src/Pure/Tools/profiling_report.scala	Tue Aug 02 16:02:06 2022 +0200
@@ -19,7 +19,7 @@
 
     using(store.open_database_context()) { db_context =>
       val result =
-        db_context.input_database(session)((db, name) => Some(store.read_theories(db, name)))
+        db_context.input_database(session)(db => Some(store.read_theories(db, session)))
       result match {
         case None => error("Missing build database for session " + quote(session))
         case Some(used_theories) =>