src/Pure/Thy/export.scala
changeset 69671 2486792eaf61
parent 69635 95dc926fa39c
child 69756 1907222d974e
     1.1 --- a/src/Pure/Thy/export.scala	Wed Jan 16 17:12:48 2019 +0100
     1.2 +++ b/src/Pure/Thy/export.scala	Wed Jan 16 17:55:26 2019 +0100
     1.3 @@ -259,6 +259,7 @@
     1.4      session_name: String,
     1.5      export_dir: Path,
     1.6      progress: Progress = No_Progress,
     1.7 +    export_prune: Int = 0,
     1.8      export_list: Boolean = false,
     1.9      export_patterns: List[String] = Nil,
    1.10      export_prefix: String = "")
    1.11 @@ -287,7 +288,13 @@
    1.12              name <- group.map(_._2).sorted
    1.13              entry <- read_entry(db, session_name, theory_name, name)
    1.14            } {
    1.15 -            val path = export_dir + Path.basic(theory_name) + Path.explode(name)
    1.16 +            val elems = theory_name :: space_explode('/', name)
    1.17 +            val path =
    1.18 +              if (elems.length < export_prune + 1) {
    1.19 +                error("Cannot prune path by " + export_prune + " element(s): " + Path.make(elems))
    1.20 +              }
    1.21 +              else export_dir + Path.make(elems.drop(export_prune))
    1.22 +
    1.23              progress.echo(export_prefix + "export " + path)
    1.24              Isabelle_System.mkdirs(path.dir)
    1.25              Bytes.write(path, entry.uncompressed(cache = store.xz_cache))
    1.26 @@ -311,6 +318,7 @@
    1.27      var export_list = false
    1.28      var no_build = false
    1.29      var options = Options.init()
    1.30 +    var export_prune = 0
    1.31      var system_mode = false
    1.32      var export_patterns: List[String] = Nil
    1.33  
    1.34 @@ -323,6 +331,7 @@
    1.35      -l           list exports
    1.36      -n           no build of session
    1.37      -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)
    1.38 +    -p NUM       prune path of exported files by NUM elements
    1.39      -s           system build mode for session image
    1.40      -x PATTERN   extract files matching pattern (e.g. "*:**" for all)
    1.41  
    1.42 @@ -338,6 +347,7 @@
    1.43        "l" -> (_ => export_list = true),
    1.44        "n" -> (_ => no_build = true),
    1.45        "o:" -> (arg => options = options + arg),
    1.46 +      "p:" -> (arg => export_prune = Value.Int.parse(arg)),
    1.47        "s" -> (_ => system_mode = true),
    1.48        "x:" -> (arg => export_patterns ::= arg))
    1.49  
    1.50 @@ -366,7 +376,7 @@
    1.51      /* export files */
    1.52  
    1.53      val store = Sessions.store(options, system_mode)
    1.54 -    export_files(store, session_name, export_dir, progress = progress,
    1.55 +    export_files(store, session_name, export_dir, progress = progress, export_prune = export_prune,
    1.56        export_list = export_list, export_patterns = export_patterns)
    1.57    })
    1.58  }