--- a/src/Pure/Tools/profiling_report.scala Sat Aug 06 16:37:23 2022 +0200
+++ b/src/Pure/Tools/profiling_report.scala Sat Aug 06 16:54:01 2022 +0200
@@ -17,8 +17,9 @@
): Unit = {
val store = Sessions.store(options)
- using(store.open_database_context()) { db_context =>
- db_context.database(session)(db => Some(store.read_theories(db, session))) match {
+ using(Export.open_session_context0(store, session)) { session_context =>
+ session_context.db_context.database(session)(db => Some(store.read_theories(db, session)))
+ match {
case None => error("Missing build database for session " + quote(session))
case Some(used_theories) =>
theories.filterNot(used_theories.toSet) match {
@@ -29,7 +30,7 @@
(for {
thy <- used_theories.iterator
if theories.isEmpty || theories.contains(thy)
- command <- Build_Job.read_session_theory(db_context, session, thy).iterator
+ command <- Build_Job.read_theory(session_context.theory(thy)).iterator
snapshot = Document.State.init.snippet(command)
(Protocol.ML_Profiling(report), _) <- snapshot.messages.iterator
} yield if (clean_name) report.clean_name else report).toList