src/Pure/Thy/export.scala

   def export_files(
     store: Sessions.Store,
     session_name: String,
     export_dir: Path,
     progress: Progress = No_Progress,
+    export_prune: Int = 0,
     export_list: Boolean = false,
     export_patterns: List[String] = Nil,
     export_prefix: String = "")
   {
     using(store.open_database(session_name))(db =>

           for {
             (theory_name, group) <- exports.toList.groupBy(_._1).toList.sortBy(_._1)
             name <- group.map(_._2).sorted
             entry <- read_entry(db, session_name, theory_name, name)
           } {
-            val path = export_dir + Path.basic(theory_name) + Path.explode(name)
+            val elems = theory_name :: space_explode('/', 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))
+
             progress.echo(export_prefix + "export " + path)
             Isabelle_System.mkdirs(path.dir)
             Bytes.write(path, entry.uncompressed(cache = store.xz_cache))
           }
         }

     var export_dir = default_export_dir
     var dirs: List[Path] = Nil
     var export_list = false
     var no_build = false
     var options = Options.init()
+    var export_prune = 0
     var system_mode = false
     var export_patterns: List[String] = Nil
 
     val getopts = Getopts("""
 Usage: isabelle export [OPTIONS] SESSION

     -O DIR       output directory for exported files (default: """ + default_export_dir + """)
     -d DIR       include session directory
     -l           list exports
     -n           no build of session
     -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)
+    -p NUM       prune path of exported files by NUM elements
     -s           system build mode for session image
     -x PATTERN   extract files matching pattern (e.g. "*:**" for all)
 
   List or export theory exports for SESSION: named blobs produced by
   isabelle build. Option -l or -x is required; option -x may be repeated.

       "O:" -> (arg => export_dir = Path.explode(arg)),
       "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))),
       "l" -> (_ => export_list = true),
       "n" -> (_ => no_build = true),
       "o:" -> (arg => options = options + arg),
+      "p:" -> (arg => export_prune = Value.Int.parse(arg)),
       "s" -> (_ => system_mode = true),
       "x:" -> (arg => export_patterns ::= arg))
 
     val more_args = getopts(args)
     val session_name =

 
 
     /* export files */
 
     val store = Sessions.store(options, system_mode)
-    export_files(store, session_name, export_dir, progress = progress,
+    export_files(store, session_name, export_dir, progress = progress, export_prune = export_prune,
       export_list = export_list, export_patterns = export_patterns)
   })
 }