guard result exports via export_pattern -- avoid bombing client via huge blobs;

--- a/src/Doc/System/Server.thy	Fri May 11 20:22:20 2018 +0200
+++ b/src/Doc/System/Server.thy	Fri May 11 20:35:29 2018 +0200
@@ -892,8 +892,9 @@
   \quad\<open>{session_id: uuid,\<close> \\
   \quad~~\<open>theories: [string],\<close> \\
   \quad~~\<open>master_dir?: string,\<close> & \<^bold>\<open>default:\<close> session \<open>tmp_dir\<close> \\
-  \quad~~\<open>pretty_margin?: double\<close> & \<^bold>\<open>default:\<close> \<^verbatim>\<open>76\<close> \\
-  \quad~~\<open>unicode_symbols?: bool}\<close> \\[2ex]
+  \quad~~\<open>pretty_margin?: double,\<close> & \<^bold>\<open>default:\<close> \<^verbatim>\<open>76\<close> \\
+  \quad~~\<open>unicode_symbols?: bool,\<close> \\
+  \quad~~\<open>export_pattern?: string}\<close> \\[2ex]
   \end{tabular}
 
   \begin{tabular}{ll}
@@ -921,13 +922,13 @@
   that with different values for \<open>pretty_margin\<close> or \<open>unicode_symbols\<close> to get
   different formatting for \<open>errors\<close> or \<open>messages\<close>.
 
-  The \<open>exports\<close> can be arbitrary binary resources produced by a theory. An
-  \<open>export\<close> \<open>name\<close> roughly follows file-system standards: ``\<^verbatim>\<open>/\<close>'' separated
-  list of base names (excluding special names like ``\<^verbatim>\<open>.\<close>'' or ``\<^verbatim>\<open>..\<close>''). The
-  \<open>base64\<close> field specifies the format of the \<open>body\<close> string: it is true for a
-  byte vector that cannot be represented as plain text in UTF-8 encoding,
-  which means the string needs to be decoded as in
-  \<^verbatim>\<open>java.util.Base64.getDecoder.decode(String)\<close>.
+  \<^medskip> A non-empty \<open>export_pattern\<close> means that theory \<open>exports\<close> are retrieved
+  (see \secref{sec:tool-export}). An \<open>export\<close> \<open>name\<close> roughly follows
+  file-system standards: ``\<^verbatim>\<open>/\<close>'' separated list of base names (excluding
+  special names like ``\<^verbatim>\<open>.\<close>'' or ``\<^verbatim>\<open>..\<close>''). The \<open>base64\<close> field specifies the
+  format of the \<open>body\<close> string: it is true for a byte vector that cannot be
+  represented as plain text in UTF-8 encoding, which means the string needs to
+  be decoded as in \<^verbatim>\<open>java.util.Base64.getDecoder.decode(String)\<close>.
 \<close>
 
 

--- a/src/Doc/System/Sessions.thy	Fri May 11 20:22:20 2018 +0200
+++ b/src/Doc/System/Sessions.thy	Fri May 11 20:35:29 2018 +0200
@@ -546,7 +546,7 @@
 \<close>
 
 
-section \<open>Retrieve theory exports\<close>
+section \<open>Retrieve theory exports \label{sec:tool-export}\<close>
 
 text \<open>
   The @{tool_def "export"} tool retrieves theory exports from the session

--- a/src/Pure/Tools/server_commands.scala	Fri May 11 20:22:20 2018 +0200
+++ b/src/Pure/Tools/server_commands.scala	Fri May 11 20:35:29 2018 +0200
@@ -156,7 +156,8 @@
       theories: List[String],
       master_dir: String = "",
       pretty_margin: Double = Pretty.default_margin,
-      unicode_symbols: Boolean = false)
+      unicode_symbols: Boolean = false,
+      export_pattern: String = "")
 
     def unapply(json: JSON.T): Option[Args] =
       for {
@@ -165,10 +166,11 @@
         master_dir <- JSON.string_default(json, "master_dir")
         pretty_margin <- JSON.double_default(json, "pretty_margin", Pretty.default_margin)
         unicode_symbols <- JSON.bool_default(json, "unicode_symbols")
+        export_pattern <- JSON.string_default(json, "export_pattern")
       }
       yield {
-        Args(session_id, theories, master_dir = master_dir,
-          pretty_margin = pretty_margin, unicode_symbols)
+        Args(session_id, theories, master_dir = master_dir, pretty_margin = pretty_margin,
+          unicode_symbols = unicode_symbols, export_pattern = export_pattern)
       }
 
     def command(args: Args,
@@ -214,11 +216,14 @@
                     (tree, pos) <- result.messages(name) if Protocol.is_exported(tree)
                   } yield output_message(tree, pos))) +
                 ("exports" ->
-                  (for { entry <- result.exports(name) }
-                   yield {
-                     val (base64, body) = entry.body.join.maybe_base64
-                     JSON.Object("name" -> entry.name, "base64" -> base64, "body" -> body)
-                   }))))
+                  (if (args.export_pattern == "") Nil else {
+                    val matcher = Export.make_matcher(args.export_pattern)
+                    for { entry <- result.exports(name) if matcher(entry.theory_name, entry.name) }
+                    yield {
+                      val (base64, body) = entry.body.join.maybe_base64
+                      JSON.Object("name" -> entry.name, "base64" -> base64, "body" -> body)
+                    }
+                  }))))
 
       (result_json, result)
     }