# HG changeset patch
# User wenzelm
# Date 1525714855 -7200
# Node ID a514e29db9806aa874b80e4e1ebbba9e0b29f913
# Parent  577072a0ceed347e9d534b18435832446616e721
return exports as result for Isabelle server;

diff -r 577072a0ceed -r a514e29db980 src/Doc/System/Server.thy
--- a/src/Doc/System/Server.thy	Mon May 07 18:25:26 2018 +0200
+++ b/src/Doc/System/Server.thy	Mon May 07 19:40:55 2018 +0200
@@ -897,10 +897,14 @@
   \end{tabular}
 
   \begin{tabular}{ll}
+  \<^bold>\<open>type\<close> \<open>export =\<close> \\
+  \quad~~\<open>{name: string, base64: bool, body: string}\<close> \\
+  \<^bold>\<open>type\<close> \<open>node_results =\<close> \\
+  \quad~~\<open>{status: node_status, messages: [message], exports: [export]}\<close> \\
   \<^bold>\<open>type\<close> \<open>use_theories_results =\<close> \\
   \quad\<open>{ok: bool,\<close> \\
   \quad~~\<open>errors: [message],\<close> \\
-  \quad~~\<open>nodes: [node \<oplus> {status: node_status, messages: [message]}]}\<close> \\
+  \quad~~\<open>nodes: [node \<oplus> node_results]}\<close> \\
   \end{tabular}
 
   \<^medskip>
@@ -916,6 +920,14 @@
   invocations of \<^verbatim>\<open>use_theories\<close> are idempotent: it could make sense to do
   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>.
 \<close>
 
 
diff -r 577072a0ceed -r a514e29db980 src/Pure/General/bytes.scala
--- a/src/Pure/General/bytes.scala	Mon May 07 18:25:26 2018 +0200
+++ b/src/Pure/General/bytes.scala	Mon May 07 19:40:55 2018 +0200
@@ -160,6 +160,12 @@
     Base64.getEncoder.encodeToString(b)
   }
 
+  def maybe_base64: (Boolean, String) =
+  {
+    val s = text
+    if (this == Bytes(s)) (false, s) else (true, base64)
+  }
+
   override def toString: String =
   {
     val str = text
diff -r 577072a0ceed -r a514e29db980 src/Pure/Thy/thy_resources.scala
--- a/src/Pure/Thy/thy_resources.scala	Mon May 07 18:25:26 2018 +0200
+++ b/src/Pure/Thy/thy_resources.scala	Mon May 07 19:40:55 2018 +0200
@@ -72,6 +72,16 @@
         (_, tree) <- state.command_results(version, command).iterator
        } yield (tree, pos)).toList
     }
+
+    def exports(node_name: Document.Node.Name): List[Export.Entry] =
+    {
+      val node = version.nodes(node_name)
+      Command.Exports.merge(
+        for {
+          command <- node.commands.iterator
+          st <- state.command_states(version, command).iterator
+        } yield st.exports).iterator.map(_._2).toList
+    }
   }
 
   class Session private[Thy_Resources](
diff -r 577072a0ceed -r a514e29db980 src/Pure/Tools/server_commands.scala
--- a/src/Pure/Tools/server_commands.scala	Mon May 07 18:25:26 2018 +0200
+++ b/src/Pure/Tools/server_commands.scala	Mon May 07 19:40:55 2018 +0200
@@ -212,7 +212,13 @@
                 ("messages" ->
                   (for {
                     (tree, pos) <- result.messages(name) if Protocol.is_exported(tree)
-                  } yield output_message(tree, pos)))))
+                  } 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)
+                   }))))
 
       (result_json, result)
     }