support pruning of export names;
authorwenzelm
Wed Jan 16 17:55:26 2019 +0100 (10 months ago)
changeset 696712486792eaf61
parent 69670 114ae60c4be7
child 69672 f97fbb2330aa
support pruning of export names;
src/Doc/System/Sessions.thy
src/Pure/Thy/export.scala
src/Pure/Thy/sessions.ML
src/Pure/Thy/sessions.scala
src/Pure/Tools/build.scala
     1.1 --- a/src/Doc/System/Sessions.thy	Wed Jan 16 17:12:48 2019 +0100
     1.2 +++ b/src/Doc/System/Sessions.thy	Wed Jan 16 17:55:26 2019 +0100
     1.3 @@ -76,7 +76,8 @@
     1.4      ;
     1.5      document_files: @'document_files' ('(' dir ')')? (@{syntax embedded}+)
     1.6      ;
     1.7 -    export_files: @'export_files' ('(' dir ')')? (@{syntax embedded}+)
     1.8 +    export_files: @'export_files' ('(' dir ')')? ('[' nat ']')? \<newline>
     1.9 +      (@{syntax embedded}+)
    1.10    \<close>
    1.11  
    1.12    \<^descr> \isakeyword{session}~\<open>A = B + body\<close> defines a new session \<open>A\<close> based on
    1.13 @@ -143,11 +144,14 @@
    1.14    original directory hierarchy of \<open>base_dir\<close>. The default \<open>base_dir\<close> is
    1.15    \<^verbatim>\<open>document\<close> within the session root directory.
    1.16  
    1.17 -  \<^descr> \isakeyword{export_files}~\<open>(\<close>\isakeyword{in}~\<open>target_dir) patterns\<close> writes
    1.18 -  theory exports to the file-system: the \<open>target_dir\<close> specification is
    1.19 -  relative to the session root directory; its default is \<^verbatim>\<open>export\<close>. Exports
    1.20 -  are selected via \<open>patterns\<close> as in @{tool_ref export}
    1.21 -  (\secref{sec:tool-export}).
    1.22 +  \<^descr> \isakeyword{export_files}~\<open>(\<close>\isakeyword{in}~\<open>target_dir) [number]
    1.23 +  patterns\<close> writes theory exports to the file-system: the \<open>target_dir\<close>
    1.24 +  specification is relative to the session root directory; its default is
    1.25 +  \<^verbatim>\<open>export\<close>. Exports are selected via \<open>patterns\<close> as in @{tool_ref export}
    1.26 +  (\secref{sec:tool-export}). The number given in brackets (default: 0)
    1.27 +  specifies elements that should be pruned from each name: it allows to reduce
    1.28 +  the resulting directory hierarchy at the danger of overwriting files due to
    1.29 +  loss of uniqueness.
    1.30  \<close>
    1.31  
    1.32  
    1.33 @@ -563,6 +567,7 @@
    1.34      -l           list exports
    1.35      -n           no build of session
    1.36      -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)
    1.37 +    -p NUM       prune path of exported files by NUM elements
    1.38      -s           system build mode for session image
    1.39      -x PATTERN   extract files matching pattern (e.g.\ "*:**" for all)
    1.40  
    1.41 @@ -594,6 +599,10 @@
    1.42    Option \<^verbatim>\<open>-O\<close> specifies an alternative output directory for option \<^verbatim>\<open>-x\<close>: the
    1.43    default is \<^verbatim>\<open>export\<close> within the current directory. Each theory creates its
    1.44    own sub-directory hierarchy, using the session-qualified theory name.
    1.45 +
    1.46 +  Option \<^verbatim>\<open>-p\<close> specifies the number of elements that should be pruned from
    1.47 +  each name: it allows to reduce the resulting directory hierarchy at the
    1.48 +  danger of overwriting files due to loss of uniqueness.
    1.49  \<close>
    1.50  
    1.51  
     2.1 --- a/src/Pure/Thy/export.scala	Wed Jan 16 17:12:48 2019 +0100
     2.2 +++ b/src/Pure/Thy/export.scala	Wed Jan 16 17:55:26 2019 +0100
     2.3 @@ -259,6 +259,7 @@
     2.4      session_name: String,
     2.5      export_dir: Path,
     2.6      progress: Progress = No_Progress,
     2.7 +    export_prune: Int = 0,
     2.8      export_list: Boolean = false,
     2.9      export_patterns: List[String] = Nil,
    2.10      export_prefix: String = "")
    2.11 @@ -287,7 +288,13 @@
    2.12              name <- group.map(_._2).sorted
    2.13              entry <- read_entry(db, session_name, theory_name, name)
    2.14            } {
    2.15 -            val path = export_dir + Path.basic(theory_name) + Path.explode(name)
    2.16 +            val elems = theory_name :: space_explode('/', name)
    2.17 +            val path =
    2.18 +              if (elems.length < export_prune + 1) {
    2.19 +                error("Cannot prune path by " + export_prune + " element(s): " + Path.make(elems))
    2.20 +              }
    2.21 +              else export_dir + Path.make(elems.drop(export_prune))
    2.22 +
    2.23              progress.echo(export_prefix + "export " + path)
    2.24              Isabelle_System.mkdirs(path.dir)
    2.25              Bytes.write(path, entry.uncompressed(cache = store.xz_cache))
    2.26 @@ -311,6 +318,7 @@
    2.27      var export_list = false
    2.28      var no_build = false
    2.29      var options = Options.init()
    2.30 +    var export_prune = 0
    2.31      var system_mode = false
    2.32      var export_patterns: List[String] = Nil
    2.33  
    2.34 @@ -323,6 +331,7 @@
    2.35      -l           list exports
    2.36      -n           no build of session
    2.37      -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)
    2.38 +    -p NUM       prune path of exported files by NUM elements
    2.39      -s           system build mode for session image
    2.40      -x PATTERN   extract files matching pattern (e.g. "*:**" for all)
    2.41  
    2.42 @@ -338,6 +347,7 @@
    2.43        "l" -> (_ => export_list = true),
    2.44        "n" -> (_ => no_build = true),
    2.45        "o:" -> (arg => options = options + arg),
    2.46 +      "p:" -> (arg => export_prune = Value.Int.parse(arg)),
    2.47        "s" -> (_ => system_mode = true),
    2.48        "x:" -> (arg => export_patterns ::= arg))
    2.49  
    2.50 @@ -366,7 +376,7 @@
    2.51      /* export files */
    2.52  
    2.53      val store = Sessions.store(options, system_mode)
    2.54 -    export_files(store, session_name, export_dir, progress = progress,
    2.55 +    export_files(store, session_name, export_dir, progress = progress, export_prune = export_prune,
    2.56        export_list = export_list, export_patterns = export_patterns)
    2.57    })
    2.58  }
     3.1 --- a/src/Pure/Thy/sessions.ML	Wed Jan 16 17:12:48 2019 +0100
     3.2 +++ b/src/Pure/Thy/sessions.ML	Wed Jan 16 17:55:26 2019 +0100
     3.3 @@ -35,9 +35,13 @@
     3.4      Parse.!!! (Scan.optional in_path ("document", Position.none)
     3.5        -- Scan.repeat1 (Parse.position Parse.path));
     3.6  
     3.7 +val prune =
     3.8 +  Scan.optional (Parse.$$$ "[" |-- Parse.!!! (Parse.nat --| Parse.$$$ "]")) 0;
     3.9 +
    3.10  val export_files =
    3.11    Parse.$$$ "export_files" |--
    3.12 -    Parse.!!! (Scan.optional in_path ("export", Position.none) -- Scan.repeat1 Parse.embedded);
    3.13 +    Parse.!!!
    3.14 +      (Scan.optional in_path ("export", Position.none) -- prune -- Scan.repeat1 Parse.embedded);
    3.15  
    3.16  in
    3.17  
    3.18 @@ -95,7 +99,7 @@
    3.19              in () end);
    3.20  
    3.21          val _ =
    3.22 -          export_files |> List.app (fn (export_dir, _) =>
    3.23 +          export_files |> List.app (fn ((export_dir, _), _) =>
    3.24              ignore (Resources.check_path ctxt session_dir export_dir));
    3.25        in () end));
    3.26  
     4.1 --- a/src/Pure/Thy/sessions.scala	Wed Jan 16 17:12:48 2019 +0100
     4.2 +++ b/src/Pure/Thy/sessions.scala	Wed Jan 16 17:55:26 2019 +0100
     4.3 @@ -515,7 +515,7 @@
     4.4      theories: List[(Options, List[(String, Position.T)])],
     4.5      global_theories: List[String],
     4.6      document_files: List[(Path, Path)],
     4.7 -    export_files: List[(Path, List[String])],
     4.8 +    export_files: List[(Path, Int, List[String])],
     4.9      meta_digest: SHA1.Digest)
    4.10    {
    4.11      def deps: List[String] = parent.toList ::: imports
    4.12 @@ -568,7 +568,7 @@
    4.13          entry.document_files.map({ case (s1, s2) => (Path.explode(s1), Path.explode(s2)) })
    4.14  
    4.15        val export_files =
    4.16 -        entry.export_files.map({ case (dir, pats) => (Path.explode(dir), pats) })
    4.17 +        entry.export_files.map({ case (dir, prune, pats) => (Path.explode(dir), prune, pats) })
    4.18  
    4.19        val meta_digest =
    4.20          SHA1.digest((name, chapter, entry.parent, entry.options, entry.imports,
    4.21 @@ -831,7 +831,7 @@
    4.22      imports: List[String],
    4.23      theories: List[(List[Options.Spec], List[((String, Position.T), Boolean)])],
    4.24      document_files: List[(String, String)],
    4.25 -    export_files: List[(String, List[String])]) extends Entry
    4.26 +    export_files: List[(String, Int, List[String])]) extends Entry
    4.27    {
    4.28      def theories_no_position: List[(List[Options.Spec], List[(String, Boolean)])] =
    4.29        theories.map({ case (a, b) => (a, b.map({ case ((c, _), d) => (c, d) })) })
    4.30 @@ -870,9 +870,11 @@
    4.31          $$$(DOCUMENT_FILES) ~!
    4.32            ((in_path | success("document")) ~ rep1(path)) ^^ { case _ ~ (x ~ y) => y.map((x, _)) }
    4.33  
    4.34 +      val prune = $$$("[") ~! (nat ~ $$$("]")) ^^ { case _ ~ (x ~ _) => x } | success(0)
    4.35 +
    4.36        val export_files =
    4.37 -        $$$(EXPORT_FILES) ~! ((in_path | success("export")) ~ rep1(embedded)) ^^
    4.38 -          { case _ ~ (x ~ y) => (x, y) }
    4.39 +        $$$(EXPORT_FILES) ~! ((in_path | success("export")) ~ prune ~ rep1(embedded)) ^^
    4.40 +          { case _ ~ (x ~ y ~ z) => (x, y, z) }
    4.41  
    4.42        command(SESSION) ~!
    4.43          (position(session_name) ~
     5.1 --- a/src/Pure/Tools/build.scala	Wed Jan 16 17:12:48 2019 +0100
     5.2 +++ b/src/Pure/Tools/build.scala	Wed Jan 16 17:55:26 2019 +0100
     5.3 @@ -335,9 +335,10 @@
     5.4        Isabelle_System.rm_tree(export_tmp_dir)
     5.5  
     5.6        if (result1.ok) {
     5.7 -        for ((dir, pats) <- info.export_files) {
     5.8 +        for ((dir, prune, pats) <- info.export_files) {
     5.9            Export.export_files(store, name, info.dir + dir,
    5.10              progress = if (verbose) progress else No_Progress,
    5.11 +            export_prune = prune,
    5.12              export_patterns = pats,
    5.13              export_prefix = name + ": ")
    5.14          }