# HG changeset patch # User wenzelm # Date 1527349035 -7200 # Node ID f1f5ccc85b25c33a7e3050436e4ef2ab73d4380e # Parent c29fc61fb1b1950ede6cf276a3e04fda8d3fb8eb support multiple patterns; diff -r c29fc61fb1b1 -r f1f5ccc85b25 src/Doc/System/Sessions.thy --- a/src/Doc/System/Sessions.thy Sat May 26 16:52:03 2018 +0200 +++ b/src/Doc/System/Sessions.thy Sat May 26 17:37:15 2018 +0200 @@ -562,7 +562,7 @@ -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. + isabelle build. Option -l or -x is required; option -x may be repeated. The PATTERN language resembles glob patterns in the shell, with ? and * (both excluding ":" and "/"), ** (excluding ":"), and [abc] or [^abc], @@ -583,7 +583,8 @@ pattern. Note that wild cards ``\<^verbatim>\?\'' and ``\<^verbatim>\*\'' do not match the separators ``\<^verbatim>\:\'' and ``\<^verbatim>\/\''; the wild card \<^verbatim>\**\ matches over directory name hierarchies separated by ``\<^verbatim>\/\''. Thus the pattern ``\<^verbatim>\*:**\'' matches - \<^emph>\all\ theory exports. + \<^emph>\all\ theory exports. Multiple options \<^verbatim>\-x\ refer to the union of all + specified patterns. Option \<^verbatim>\-D\ specifies an alternative base directory for option \<^verbatim>\-x\: the default is \<^verbatim>\export\ within the current directory. Each theory creates its diff -r c29fc61fb1b1 -r f1f5ccc85b25 src/Pure/Thy/export.scala --- a/src/Pure/Thy/export.scala Sat May 26 16:52:03 2018 +0200 +++ b/src/Pure/Thy/export.scala Sat May 26 17:37:15 2018 +0200 @@ -193,7 +193,7 @@ export_dir: Path, progress: Progress = No_Progress, export_list: Boolean = false, - export_pattern: String = "") + export_patterns: List[String] = Nil) { using(store.open_database(session_name))(db => { @@ -207,10 +207,16 @@ } // export - if (export_pattern != "") { - val matcher = make_matcher(export_pattern) + if (export_patterns.nonEmpty) { + val exports = + (for { + export_pattern <- export_patterns.iterator + matcher = make_matcher(export_pattern) + (theory_name, name) <- export_names if matcher(theory_name, name) + } yield (theory_name, name)).toSet for { - (theory_name, name) <- export_names if matcher(theory_name, name) + (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) @@ -238,7 +244,7 @@ var no_build = false var options = Options.init() var system_mode = false - var export_pattern = "" + var export_patterns: List[String] = Nil val getopts = Getopts(""" Usage: isabelle export [OPTIONS] SESSION @@ -253,7 +259,7 @@ -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. + isabelle build. Option -l or -x is required; option -x may be repeated. The PATTERN language resembles glob patterns in the shell, with ? and * (both excluding ":" and "/"), ** (excluding ":"), and [abc] or [^abc], @@ -265,12 +271,12 @@ "n" -> (_ => no_build = true), "o:" -> (arg => options = options + arg), "s" -> (_ => system_mode = true), - "x:" -> (arg => export_pattern = arg)) + "x:" -> (arg => export_patterns ::= arg)) val more_args = getopts(args) val session_name = more_args match { - case List(session_name) if export_list || export_pattern != "" => session_name + case List(session_name) if export_list || export_patterns.nonEmpty => session_name case _ => getopts.usage() } @@ -297,6 +303,6 @@ val store = Sessions.store(options, system_mode) export_files(store, session_name, export_dir, progress = progress, - export_list = export_list, export_pattern = export_pattern) + export_list = export_list, export_patterns = export_patterns) }) }