guard result exports via export_pattern -- avoid bombing client via huge blobs;
authorwenzelm
Fri May 11 20:35:29 2018 +0200 (12 months ago)
changeset 68152619de043389f
parent 68151 3c321783bae3
child 68153 e469d529e6da
guard result exports via export_pattern -- avoid bombing client via huge blobs;
src/Doc/System/Server.thy
src/Doc/System/Sessions.thy
src/Pure/Tools/server_commands.scala
     1.1 --- a/src/Doc/System/Server.thy	Fri May 11 20:22:20 2018 +0200
     1.2 +++ b/src/Doc/System/Server.thy	Fri May 11 20:35:29 2018 +0200
     1.3 @@ -892,8 +892,9 @@
     1.4    \quad\<open>{session_id: uuid,\<close> \\
     1.5    \quad~~\<open>theories: [string],\<close> \\
     1.6    \quad~~\<open>master_dir?: string,\<close> & \<^bold>\<open>default:\<close> session \<open>tmp_dir\<close> \\
     1.7 -  \quad~~\<open>pretty_margin?: double\<close> & \<^bold>\<open>default:\<close> \<^verbatim>\<open>76\<close> \\
     1.8 -  \quad~~\<open>unicode_symbols?: bool}\<close> \\[2ex]
     1.9 +  \quad~~\<open>pretty_margin?: double,\<close> & \<^bold>\<open>default:\<close> \<^verbatim>\<open>76\<close> \\
    1.10 +  \quad~~\<open>unicode_symbols?: bool,\<close> \\
    1.11 +  \quad~~\<open>export_pattern?: string}\<close> \\[2ex]
    1.12    \end{tabular}
    1.13  
    1.14    \begin{tabular}{ll}
    1.15 @@ -921,13 +922,13 @@
    1.16    that with different values for \<open>pretty_margin\<close> or \<open>unicode_symbols\<close> to get
    1.17    different formatting for \<open>errors\<close> or \<open>messages\<close>.
    1.18  
    1.19 -  The \<open>exports\<close> can be arbitrary binary resources produced by a theory. An
    1.20 -  \<open>export\<close> \<open>name\<close> roughly follows file-system standards: ``\<^verbatim>\<open>/\<close>'' separated
    1.21 -  list of base names (excluding special names like ``\<^verbatim>\<open>.\<close>'' or ``\<^verbatim>\<open>..\<close>''). The
    1.22 -  \<open>base64\<close> field specifies the format of the \<open>body\<close> string: it is true for a
    1.23 -  byte vector that cannot be represented as plain text in UTF-8 encoding,
    1.24 -  which means the string needs to be decoded as in
    1.25 -  \<^verbatim>\<open>java.util.Base64.getDecoder.decode(String)\<close>.
    1.26 +  \<^medskip> A non-empty \<open>export_pattern\<close> means that theory \<open>exports\<close> are retrieved
    1.27 +  (see \secref{sec:tool-export}). An \<open>export\<close> \<open>name\<close> roughly follows
    1.28 +  file-system standards: ``\<^verbatim>\<open>/\<close>'' separated list of base names (excluding
    1.29 +  special names like ``\<^verbatim>\<open>.\<close>'' or ``\<^verbatim>\<open>..\<close>''). The \<open>base64\<close> field specifies the
    1.30 +  format of the \<open>body\<close> string: it is true for a byte vector that cannot be
    1.31 +  represented as plain text in UTF-8 encoding, which means the string needs to
    1.32 +  be decoded as in \<^verbatim>\<open>java.util.Base64.getDecoder.decode(String)\<close>.
    1.33  \<close>
    1.34  
    1.35  
     2.1 --- a/src/Doc/System/Sessions.thy	Fri May 11 20:22:20 2018 +0200
     2.2 +++ b/src/Doc/System/Sessions.thy	Fri May 11 20:35:29 2018 +0200
     2.3 @@ -546,7 +546,7 @@
     2.4  \<close>
     2.5  
     2.6  
     2.7 -section \<open>Retrieve theory exports\<close>
     2.8 +section \<open>Retrieve theory exports \label{sec:tool-export}\<close>
     2.9  
    2.10  text \<open>
    2.11    The @{tool_def "export"} tool retrieves theory exports from the session
     3.1 --- a/src/Pure/Tools/server_commands.scala	Fri May 11 20:22:20 2018 +0200
     3.2 +++ b/src/Pure/Tools/server_commands.scala	Fri May 11 20:35:29 2018 +0200
     3.3 @@ -156,7 +156,8 @@
     3.4        theories: List[String],
     3.5        master_dir: String = "",
     3.6        pretty_margin: Double = Pretty.default_margin,
     3.7 -      unicode_symbols: Boolean = false)
     3.8 +      unicode_symbols: Boolean = false,
     3.9 +      export_pattern: String = "")
    3.10  
    3.11      def unapply(json: JSON.T): Option[Args] =
    3.12        for {
    3.13 @@ -165,10 +166,11 @@
    3.14          master_dir <- JSON.string_default(json, "master_dir")
    3.15          pretty_margin <- JSON.double_default(json, "pretty_margin", Pretty.default_margin)
    3.16          unicode_symbols <- JSON.bool_default(json, "unicode_symbols")
    3.17 +        export_pattern <- JSON.string_default(json, "export_pattern")
    3.18        }
    3.19        yield {
    3.20 -        Args(session_id, theories, master_dir = master_dir,
    3.21 -          pretty_margin = pretty_margin, unicode_symbols)
    3.22 +        Args(session_id, theories, master_dir = master_dir, pretty_margin = pretty_margin,
    3.23 +          unicode_symbols = unicode_symbols, export_pattern = export_pattern)
    3.24        }
    3.25  
    3.26      def command(args: Args,
    3.27 @@ -214,11 +216,14 @@
    3.28                      (tree, pos) <- result.messages(name) if Protocol.is_exported(tree)
    3.29                    } yield output_message(tree, pos))) +
    3.30                  ("exports" ->
    3.31 -                  (for { entry <- result.exports(name) }
    3.32 -                   yield {
    3.33 -                     val (base64, body) = entry.body.join.maybe_base64
    3.34 -                     JSON.Object("name" -> entry.name, "base64" -> base64, "body" -> body)
    3.35 -                   }))))
    3.36 +                  (if (args.export_pattern == "") Nil else {
    3.37 +                    val matcher = Export.make_matcher(args.export_pattern)
    3.38 +                    for { entry <- result.exports(name) if matcher(entry.theory_name, entry.name) }
    3.39 +                    yield {
    3.40 +                      val (base64, body) = entry.body.join.maybe_base64
    3.41 +                      JSON.Object("name" -> entry.name, "base64" -> base64, "body" -> body)
    3.42 +                    }
    3.43 +                  }))))
    3.44  
    3.45        (result_json, result)
    3.46      }