--- 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
--- 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>
--- 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 [];
--- 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))
--- 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)
})
}
--- 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));
--- 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) ~
--- 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 + ": ")
}