--- a/src/Pure/Thy/export.scala Mon Jul 11 14:56:30 2022 +0200
+++ b/src/Pure/Thy/export.scala Mon Jul 11 15:08:57 2022 +0200
@@ -54,6 +54,14 @@
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] = {
+ 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)
+ }
+
def readable(db: SQL.Database): Boolean = {
val select = Data.table.select(List(Data.name), Data.where_equal(session, theory, name))
db.using_statement(select)(stmt => stmt.execute_query().next())
@@ -361,13 +369,7 @@
entry_name <- entry_names if matcher(entry_name)
entry <- entry_name.read(db, store.cache)
} {
- val elems = entry_name.theory :: space_explode('/', entry_name.name)
- val path =
- if (elems.length < export_prune + 1) {
- error("Cannot prune path by " + export_prune + " element(s): " + Path.make(elems))
- }
- else export_dir + Path.make(elems.drop(export_prune))
-
+ val path = export_dir + Path.make(entry_name.elements(prune = export_prune))
progress.echo("export " + path + (if (entry.executable) " (executable)" else ""))
Isabelle_System.make_directory(path.dir)
val bytes = entry.uncompressed