src/Pure/PIDE/resources.scala
changeset 73565 1aa92bc4d356
parent 73359 d8a0e996614b
child 74671 df12779c3ce8
--- a/src/Pure/PIDE/resources.scala	Mon Apr 12 15:00:03 2021 +0200
+++ b/src/Pure/PIDE/resources.scala	Mon Apr 12 18:10:13 2021 +0200
@@ -39,14 +39,14 @@
       pair(list(pair(string, string)),
       pair(list(pair(string, list(string))),
       pair(list(properties),
-      pair(list(pair(string, properties)),
+      pair(list(pair(string, pair(bool, properties))),
       pair(list(pair(string, string)), list(string))))))))(
        (sessions_structure.session_positions,
        (sessions_structure.dest_session_directories,
        (sessions_structure.session_chapters,
        (sessions_structure.bibtex_entries,
        (command_timings,
-       (Scala.functions.map(fun => (fun.name, fun.position)),
+       (Scala.functions.map(fun => (fun.name, (fun.multi, fun.position))),
        (session_base.global_theories.toList,
         session_base.loaded_theories.keys)))))))))
   }