src/Pure/PIDE/resources.scala

--- a/src/Pure/PIDE/resources.scala	Tue Nov 17 22:05:59 2020 +0100
+++ b/src/Pure/PIDE/resources.scala	Tue Nov 17 22:57:56 2020 +0100
@@ -15,7 +15,8 @@
 class Resources(
   val sessions_structure: Sessions.Structure,
   val session_base: Sessions.Base,
-  val log: Logger = No_Logger)
+  val log: Logger = No_Logger,
+  command_timings: List[Properties.T] = Nil)
 {
   resources =>
 
@@ -32,16 +33,18 @@
       pair(list(pair(string, string)),
       pair(list(pair(string, string)),
       pair(list(pair(string, list(string))),
+      pair(list(properties),
       pair(list(string),
-      pair(list(pair(string, string)), list(string))))))))(
+      pair(list(pair(string, string)), list(string)))))))))(
        (Symbol.codes,
        (resources.sessions_structure.session_positions,
        (resources.sessions_structure.dest_session_directories,
        (resources.sessions_structure.session_chapters,
        (resources.sessions_structure.bibtex_entries,
+       (command_timings,
        (resources.session_base.doc_names,
        (resources.session_base.global_theories.toList,
-        resources.session_base.loaded_theories.keys)))))))))
+        resources.session_base.loaded_theories.keys))))))))))
   }