# HG changeset patch
# User wenzelm
# Date 1525552415 -7200
# Node ID 0763d4eb3ebc861b83dc175deac8701341f86df2
# Parent  dac267cd51fe3dd9fdab2c63da4f16927a53303e
protocol message for export of theory resources;

diff -r dac267cd51fe -r 0763d4eb3ebc src/Pure/PIDE/markup.ML
--- a/src/Pure/PIDE/markup.ML	Sat May 05 21:44:18 2018 +0200
+++ b/src/Pure/PIDE/markup.ML	Sat May 05 22:33:35 2018 +0200
@@ -202,6 +202,8 @@
   val task_statistics: Properties.entry
   val command_timing: Properties.entry
   val theory_timing: Properties.entry
+  val exportN: string
+  val export: {id: string option, theory_name: string, path: string, compress: bool} -> Properties.T
   val loading_theory: string -> Properties.T
   val dest_loading_theory: Properties.T -> string option
   val build_session_finished: Properties.T
@@ -638,6 +640,11 @@
 
 val theory_timing = (functionN, "theory_timing");
 
+val exportN = "export";
+fun export {id, theory_name, path, compress} =
+  [(functionN, exportN), ("id", the_default "" id),
+    ("theory_name", theory_name), ("path", path), ("compress", Value.print_bool compress)];
+
 fun loading_theory name = [("function", "loading_theory"), ("name", name)];
 
 fun dest_loading_theory [("function", "loading_theory"), ("name", name)] = SOME name
diff -r dac267cd51fe -r 0763d4eb3ebc src/Pure/PIDE/markup.scala
--- a/src/Pure/PIDE/markup.scala	Sat May 05 21:44:18 2018 +0200
+++ b/src/Pure/PIDE/markup.scala	Sat May 05 22:33:35 2018 +0200
@@ -568,6 +568,32 @@
       }
   }
 
+  val EXPORT = "export"
+  object Export
+  {
+    sealed case class Args(id: Option[String], theory_name: String, path: String, compress: Boolean)
+
+    val THEORY_NAME = "theory_name"
+    val PATH = "path"
+    val COMPRESS = "compress"
+
+    def dest_inline(props: Properties.T): Option[(Args, Bytes)] =
+      props match {
+        case
+          List((THEORY_NAME, theory_name), (PATH, path), (COMPRESS, Value.Boolean(compress)),
+            (EXPORT, hex)) => Some((Args(None, theory_name, path, compress), Bytes.hex(hex)))
+        case _ => None
+      }
+
+    def unapply(props: Properties.T): Option[Args] =
+      props match {
+        case List((FUNCTION, EXPORT), (ID, id),
+          (THEORY_NAME, theory_name), (PATH, path), (COMPRESS, Value.Boolean(compress))) =>
+            Some(Args(proper_string(id), theory_name, path, compress))
+        case _ => None
+      }
+  }
+
   val BUILD_SESSION_FINISHED = "build_session_finished"
   val Build_Session_Finished: Properties.T = List((FUNCTION, BUILD_SESSION_FINISHED))
 
diff -r dac267cd51fe -r 0763d4eb3ebc src/Pure/PIDE/resources.ML
--- a/src/Pure/PIDE/resources.ML	Sat May 05 21:44:18 2018 +0200
+++ b/src/Pure/PIDE/resources.ML	Sat May 05 22:33:35 2018 +0200
@@ -36,6 +36,7 @@
   val check_path: Proof.context -> Path.T -> string * Position.T -> Path.T
   val check_file: Proof.context -> Path.T -> string * Position.T -> Path.T
   val check_dir: Proof.context -> Path.T -> string * Position.T -> Path.T
+  val export: {theory_name: string, path: string, compress: bool} -> Output.output list -> unit
 end;
 
 structure Resources: RESOURCES =
@@ -295,4 +296,15 @@
 
 end;
 
+
+(* export *)
+
+fun export {theory_name, path, compress} output =
+  let
+    val props =
+      Markup.export
+        {id = Position.get_id (Position.thread_data ()),
+          theory_name = theory_name, path = path, compress = compress};
+  in Output.try_protocol_message props output end;
+
 end;
diff -r dac267cd51fe -r 0763d4eb3ebc src/Pure/PIDE/session.scala
--- a/src/Pure/PIDE/session.scala	Sat May 05 21:44:18 2018 +0200
+++ b/src/Pure/PIDE/session.scala	Sat May 05 22:33:35 2018 +0200
@@ -435,6 +435,9 @@
               case Protocol.Theory_Timing(_, _) =>
                 // FIXME
 
+              case Markup.Export(_) =>
+                // FIXME
+
               case Markup.Assign_Update =>
                 msg.text match {
                   case Protocol.Assign_Update(id, update) =>
diff -r dac267cd51fe -r 0763d4eb3ebc src/Pure/Tools/build.ML
--- a/src/Pure/Tools/build.ML	Sat May 05 21:44:18 2018 +0200
+++ b/src/Pure/Tools/build.ML	Sat May 05 22:33:35 2018 +0200
@@ -94,6 +94,10 @@
         end
       else if function = Markup.theory_timing then
         inline_message (#2 function) args
+      else if function = (Markup.functionN, Markup.exportN) andalso
+        not (null args) andalso #1 (hd args) = Markup.idN
+      then
+        inline_message (#2 function) (tl args @ [(Markup.exportN, hex_string (implode output))])
       else
         (case Markup.dest_loading_theory props of
           SOME name => writeln ("\floading_theory = " ^ name)
diff -r dac267cd51fe -r 0763d4eb3ebc src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Sat May 05 21:44:18 2018 +0200
+++ b/src/Pure/Tools/build.scala	Sat May 05 22:33:35 2018 +0200
@@ -282,6 +282,11 @@
               Library.try_unprefix("\floading_theory = ", line) match {
                 case Some(theory) => progress.theory(name, theory)
                 case None =>
+                  for {
+                    text <- Library.try_unprefix("\fexport = ", line)
+                    (args, body) <-
+                      Markup.Export.dest_inline(XML.Decode.properties(YXML.parse_body(text)))
+                  } { } // FIXME
               },
             progress_limit =
               options.int("process_output_limit") match {