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)