support multiple patterns;

--- 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>\<open>?\<close>'' and ``\<^verbatim>\<open>*\<close>'' do not match the
   separators ``\<^verbatim>\<open>:\<close>'' and ``\<^verbatim>\<open>/\<close>''; the wild card \<^verbatim>\<open>**\<close> matches over directory
   name hierarchies separated by ``\<^verbatim>\<open>/\<close>''. Thus the pattern ``\<^verbatim>\<open>*:**\<close>'' matches
-  \<^emph>\<open>all\<close> theory exports.
+  \<^emph>\<open>all\<close> theory exports. Multiple options \<^verbatim>\<open>-x\<close> refer to the union of all
+  specified patterns.
 
   Option \<^verbatim>\<open>-D\<close> specifies an alternative base directory for option \<^verbatim>\<open>-x\<close>: the
   default is \<^verbatim>\<open>export\<close> within the current directory. Each theory creates its

--- 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)
   })
 }