# 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)