# HG changeset patch # User wenzelm # Date 1657634655 -7200 # Node ID 605f4b6b57859a4adf2d6bff23937f8d3de3d857 # Parent aa89255b704c43309d9e58c1cadad7561ea9cd9d clarified signature; diff -r aa89255b704c -r 605f4b6b5785 src/Pure/Thy/export.scala --- a/src/Pure/Thy/export.scala Tue Jul 12 15:42:57 2022 +0200 +++ b/src/Pure/Thy/export.scala Tue Jul 12 16:04:15 2022 +0200 @@ -54,12 +54,12 @@ sealed case class Entry_Name(session: String = "", theory: String = "", name: String = "") { val compound_name: String = Export.compound_name(theory, name) - def elements(prune: Int = 0): List[String] = { + def make_path(prune: Int = 0): Path = { val elems = theory :: space_explode('/', name) if (elems.length < prune + 1) { error("Cannot prune path by " + prune + " element(s): " + Path.make(elems)) } - else elems.drop(prune) + else Path.make(elems.drop(prune)) } def readable(db: SQL.Database): Boolean = { @@ -369,7 +369,7 @@ entry_name <- entry_names if matcher(entry_name) entry <- entry_name.read(db, store.cache) } { - val path = export_dir + Path.make(entry_name.elements(prune = export_prune)) + val path = export_dir + entry_name.make_path(prune = export_prune) progress.echo("export " + path + (if (entry.executable) " (executable)" else "")) Isabelle_System.make_directory(path.dir) val bytes = entry.uncompressed diff -r aa89255b704c -r 605f4b6b5785 src/Pure/Thy/sessions.scala --- a/src/Pure/Thy/sessions.scala Tue Jul 12 15:42:57 2022 +0200 +++ b/src/Pure/Thy/sessions.scala Tue Jul 12 16:04:15 2022 +0200 @@ -1259,7 +1259,7 @@ for { entry_name <- Export.read_entry_names(db, name) if matcher(entry_name) entry <- entry_name.read(db, store.cache) - } yield File.Content(Path.make(entry.entry_name.elements()), entry.uncompressed) + } yield File.Content(entry.entry_name.make_path(), entry.uncompressed) Some(res) } ).getOrElse(Nil)