# HG changeset patch
# User wenzelm
# Date 1547661258 -3600
# Node ID cc47e7e06f383419ec8fcc465b8ea4cfe5247bc8
# Parent  de2f0a24b0f00e0b372c095615d1117958f287e3# Parent  f97fbb2330aa297d7983baeaddd8ba5a72abdaac
merged

diff -r de2f0a24b0f0 -r cc47e7e06f38 NEWS
--- a/NEWS	Wed Jan 16 17:03:31 2019 +0100
+++ b/NEWS	Wed Jan 16 18:54:18 2019 +0100
@@ -76,9 +76,10 @@
 
 * Code generation: command 'export_code' without file keyword exports
 code as regular theory export, which can be materialized using the
-command-line tool "isabelle export", or browsed in Isabelle/jEdit via
-the "isabelle-export:" file-system. To get generated code dumped into
-output, use "file \<open>\<close>". Minor INCOMPATIBILITY.
+command-line tool "isabelle export" or 'export_files' in the session
+ROOT, or browsed in Isabelle/jEdit via the "isabelle-export:"
+file-system. To get generated code dumped into output, use "file \<open>\<close>".
+Minor INCOMPATIBILITY.
 
 * Simplified syntax setup for big operators under image. In rare
 situations, type conversions are not inserted implicitly any longer
diff -r de2f0a24b0f0 -r cc47e7e06f38 src/Doc/System/Sessions.thy
--- a/src/Doc/System/Sessions.thy	Wed Jan 16 17:03:31 2019 +0100
+++ b/src/Doc/System/Sessions.thy	Wed Jan 16 18:54:18 2019 +0100
@@ -76,7 +76,8 @@
     ;
     document_files: @'document_files' ('(' dir ')')? (@{syntax embedded}+)
     ;
-    export_files: @'export_files' ('(' dir ')')? (@{syntax embedded}+)
+    export_files: @'export_files' ('(' dir ')')? ('[' nat ']')? \<newline>
+      (@{syntax embedded}+)
   \<close>
 
   \<^descr> \isakeyword{session}~\<open>A = B + body\<close> defines a new session \<open>A\<close> based on
@@ -143,11 +144,14 @@
   original directory hierarchy of \<open>base_dir\<close>. The default \<open>base_dir\<close> is
   \<^verbatim>\<open>document\<close> within the session root directory.
 
-  \<^descr> \isakeyword{export_files}~\<open>(\<close>\isakeyword{in}~\<open>target_dir) patterns\<close> writes
-  theory exports to the file-system: the \<open>target_dir\<close> specification is
-  relative to the session root directory; its default is \<^verbatim>\<open>export\<close>. Exports
-  are selected via \<open>patterns\<close> as in @{tool_ref export}
-  (\secref{sec:tool-export}).
+  \<^descr> \isakeyword{export_files}~\<open>(\<close>\isakeyword{in}~\<open>target_dir) [number]
+  patterns\<close> writes theory exports to the file-system: the \<open>target_dir\<close>
+  specification is relative to the session root directory; its default is
+  \<^verbatim>\<open>export\<close>. Exports are selected via \<open>patterns\<close> as in @{tool_ref export}
+  (\secref{sec:tool-export}). The number given in brackets (default: 0)
+  specifies elements that should be pruned from each name: it allows to reduce
+  the resulting directory hierarchy at the danger of overwriting files due to
+  loss of uniqueness.
 \<close>
 
 
@@ -563,6 +567,7 @@
     -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)
 
@@ -594,6 +599,10 @@
   Option \<^verbatim>\<open>-O\<close> specifies an alternative output directory for option \<^verbatim>\<open>-x\<close>: the
   default is \<^verbatim>\<open>export\<close> within the current directory. Each theory creates its
   own sub-directory hierarchy, using the session-qualified theory name.
+
+  Option \<^verbatim>\<open>-p\<close> specifies the number of elements that should be pruned from
+  each name: it allows to reduce the resulting directory hierarchy at the
+  danger of overwriting files due to loss of uniqueness.
 \<close>
 
 
diff -r de2f0a24b0f0 -r cc47e7e06f38 src/Pure/General/path.ML
--- a/src/Pure/General/path.ML	Wed Jan 16 17:03:31 2019 +0100
+++ b/src/Pure/General/path.ML	Wed Jan 16 18:54:18 2019 +0100
@@ -14,6 +14,7 @@
   val root: T
   val named_root: string -> T
   val parent: T
+  val make: string list -> T
   val basic: string -> T
   val variable: string -> T
   val has_parent: T -> bool
@@ -22,7 +23,6 @@
   val starts_basic: T -> bool
   val append: T -> T -> T
   val appends: T list -> T
-  val make: string list -> T
   val implode: T -> string
   val explode: string -> T
   val decode: T XML.Decode.T
@@ -88,6 +88,7 @@
 val current = Path [];
 val root = Path [Root ""];
 fun named_root s = Path [root_elem s];
+val make = Path o rev o map basic_elem;
 fun basic s = Path [basic_elem s];
 fun variable s = Path [variable_elem s];
 val parent = Path [Parent];
@@ -117,7 +118,6 @@
 
 fun append (Path xs) (Path ys) = Path (fold_rev apply ys xs);
 fun appends paths = Library.foldl (uncurry append) (current, paths);
-val make = appends o map basic;
 
 fun norm elems = fold_rev apply elems [];
 
diff -r de2f0a24b0f0 -r cc47e7e06f38 src/Pure/General/path.scala
--- a/src/Pure/General/path.scala	Wed Jan 16 17:03:31 2019 +0100
+++ b/src/Pure/General/path.scala	Wed Jan 16 18:54:18 2019 +0100
@@ -73,6 +73,7 @@
   val current: Path = new Path(Nil)
   val root: Path = new Path(List(Root("")))
   def named_root(s: String): Path = new Path(List(root_elem(s)))
+  def make(elems: List[String]): Path = new Path(elems.reverse.map(basic_elem(_)))
   def basic(s: String): Path = new Path(List(basic_elem(s)))
   def variable(s: String): Path = new Path(List(variable_elem(s)))
   val parent: Path = new Path(List(Parent))
diff -r de2f0a24b0f0 -r cc47e7e06f38 src/Pure/Thy/export.scala
--- a/src/Pure/Thy/export.scala	Wed Jan 16 17:03:31 2019 +0100
+++ b/src/Pure/Thy/export.scala	Wed Jan 16 18:54:18 2019 +0100
@@ -259,6 +259,7 @@
     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 = "")
@@ -287,7 +288,13 @@
             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))
@@ -311,6 +318,7 @@
     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
 
@@ -323,6 +331,7 @@
     -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)
 
@@ -338,6 +347,7 @@
       "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))
 
@@ -366,7 +376,7 @@
     /* 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)
   })
 }
diff -r de2f0a24b0f0 -r cc47e7e06f38 src/Pure/Thy/sessions.ML
--- a/src/Pure/Thy/sessions.ML	Wed Jan 16 17:03:31 2019 +0100
+++ b/src/Pure/Thy/sessions.ML	Wed Jan 16 18:54:18 2019 +0100
@@ -35,9 +35,13 @@
     Parse.!!! (Scan.optional in_path ("document", Position.none)
       -- Scan.repeat1 (Parse.position Parse.path));
 
+val prune =
+  Scan.optional (Parse.$$$ "[" |-- Parse.!!! (Parse.nat --| Parse.$$$ "]")) 0;
+
 val export_files =
   Parse.$$$ "export_files" |--
-    Parse.!!! (Scan.optional in_path ("export", Position.none) -- Scan.repeat1 Parse.embedded);
+    Parse.!!!
+      (Scan.optional in_path ("export", Position.none) -- prune -- Scan.repeat1 Parse.embedded);
 
 in
 
@@ -95,7 +99,7 @@
             in () end);
 
         val _ =
-          export_files |> List.app (fn (export_dir, _) =>
+          export_files |> List.app (fn ((export_dir, _), _) =>
             ignore (Resources.check_path ctxt session_dir export_dir));
       in () end));
 
diff -r de2f0a24b0f0 -r cc47e7e06f38 src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Wed Jan 16 17:03:31 2019 +0100
+++ b/src/Pure/Thy/sessions.scala	Wed Jan 16 18:54:18 2019 +0100
@@ -515,7 +515,7 @@
     theories: List[(Options, List[(String, Position.T)])],
     global_theories: List[String],
     document_files: List[(Path, Path)],
-    export_files: List[(Path, List[String])],
+    export_files: List[(Path, Int, List[String])],
     meta_digest: SHA1.Digest)
   {
     def deps: List[String] = parent.toList ::: imports
@@ -568,7 +568,7 @@
         entry.document_files.map({ case (s1, s2) => (Path.explode(s1), Path.explode(s2)) })
 
       val export_files =
-        entry.export_files.map({ case (dir, pats) => (Path.explode(dir), pats) })
+        entry.export_files.map({ case (dir, prune, pats) => (Path.explode(dir), prune, pats) })
 
       val meta_digest =
         SHA1.digest((name, chapter, entry.parent, entry.options, entry.imports,
@@ -831,7 +831,7 @@
     imports: List[String],
     theories: List[(List[Options.Spec], List[((String, Position.T), Boolean)])],
     document_files: List[(String, String)],
-    export_files: List[(String, List[String])]) extends Entry
+    export_files: List[(String, Int, List[String])]) extends Entry
   {
     def theories_no_position: List[(List[Options.Spec], List[(String, Boolean)])] =
       theories.map({ case (a, b) => (a, b.map({ case ((c, _), d) => (c, d) })) })
@@ -870,9 +870,11 @@
         $$$(DOCUMENT_FILES) ~!
           ((in_path | success("document")) ~ rep1(path)) ^^ { case _ ~ (x ~ y) => y.map((x, _)) }
 
+      val prune = $$$("[") ~! (nat ~ $$$("]")) ^^ { case _ ~ (x ~ _) => x } | success(0)
+
       val export_files =
-        $$$(EXPORT_FILES) ~! ((in_path | success("export")) ~ rep1(embedded)) ^^
-          { case _ ~ (x ~ y) => (x, y) }
+        $$$(EXPORT_FILES) ~! ((in_path | success("export")) ~ prune ~ rep1(embedded)) ^^
+          { case _ ~ (x ~ y ~ z) => (x, y, z) }
 
       command(SESSION) ~!
         (position(session_name) ~
diff -r de2f0a24b0f0 -r cc47e7e06f38 src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Wed Jan 16 17:03:31 2019 +0100
+++ b/src/Pure/Tools/build.scala	Wed Jan 16 18:54:18 2019 +0100
@@ -335,9 +335,10 @@
       Isabelle_System.rm_tree(export_tmp_dir)
 
       if (result1.ok) {
-        for ((dir, pats) <- info.export_files) {
+        for ((dir, prune, pats) <- info.export_files) {
           Export.export_files(store, name, info.dir + dir,
             progress = if (verbose) progress else No_Progress,
+            export_prune = prune,
             export_patterns = pats,
             export_prefix = name + ": ")
         }