diff -r b99b925dbd84 -r 0f8742b5a9e8 src/Pure/PIDE/resources.scala --- a/src/Pure/PIDE/resources.scala Thu Aug 29 15:43:05 2019 +0200 +++ b/src/Pure/PIDE/resources.scala Thu Aug 29 17:13:49 2019 +0200 @@ -135,6 +135,13 @@ def import_name(info: Sessions.Info, s: String): Document.Node.Name = import_name(info.name, info.dir.implode, s) + def dump_checkpoint(info: Sessions.Info): List[Document.Node.Name] = + for { + (options, thys) <- info.theories + if options.bool("dump_checkpoint") + (thy, _) <- thys + } yield import_name(info, thy) + def standard_import(base: Sessions.Base, qualifier: String, dir: String, s: String): String = { val name = import_name(qualifier, dir, s)