changeset 72622 | 830222403681 |
parent 72616 | 217e6cf61453 |
child 72626 | 5a616815cc44 |
--- a/src/Pure/Thy/sessions.scala Mon Nov 16 22:21:40 2020 +0100 +++ b/src/Pure/Thy/sessions.scala Mon Nov 16 22:23:04 2020 +0100 @@ -459,6 +459,8 @@ export_files: List[(Path, Int, List[String])], meta_digest: SHA1.Digest) { + def chapter_session: Path = Path.basic(chapter) + Path.basic(name) + def deps: List[String] = parent.toList ::: imports def deps_base(session_bases: String => Base): Base =