src/Pure/Thy/export.scala

     store: Sessions.Store,
     session_name: String,
     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 =>
     {
       db.transaction {
         val export_names = read_theory_exports(db, session_name)

           (for ((theory_name, name) <- export_names) yield compound_name(theory_name, name)).
             sorted.foreach(Output.writeln(_, stdout = true))
         }
 
         // 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)
             progress.echo("exporting " + path)
             Isabelle_System.mkdirs(path.dir)

     var dirs: List[Path] = Nil
     var export_list = false
     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
 
   Options are:

     -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)
     -s           system build mode for session image
     -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],
   and variants {pattern1,pattern2,pattern3}.
 """,

       "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))),
       "l" -> (_ => export_list = true),
       "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()
       }
 
 
     /* build */

 
     /* export files */
 
     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)
   })
 }