store exports within PIDE command state;
Markup.Export.unapply: proper NAME;

--- a/src/Pure/PIDE/command.scala	Sun May 06 23:59:14 2018 +0100
+++ b/src/Pure/PIDE/command.scala	Mon May 07 17:11:01 2018 +0200
@@ -28,7 +28,7 @@
   object Results
   {
     type Entry = (Long, XML.Tree)
-    val empty = new Results(SortedMap.empty)
+    val empty: Results = new Results(SortedMap.empty)
     def make(args: TraversableOnce[Results.Entry]): Results = (empty /: args)(_ + _)
     def merge(args: TraversableOnce[Results]): Results = (empty /: args)(_ ++ _)
 
@@ -68,7 +68,39 @@
   }
 
 
-  /* markup */
+  /* exports */
+
+  object Exports
+  {
+    type Entry = (Long, Export.Entry)
+    val empty: Exports = new Exports(SortedMap.empty)
+    def merge(args: TraversableOnce[Exports]): Exports = (empty /: args)(_ ++ _)
+  }
+
+  final class Exports private(private val rep: SortedMap[Long, Export.Entry])
+  {
+    def iterator: Iterator[Exports.Entry] = rep.iterator
+
+    def + (entry: Exports.Entry): Exports =
+      if (rep.isDefinedAt(entry._1)) this
+      else new Exports(rep + entry)
+
+    def ++ (other: Exports): Exports =
+      if (this eq other) this
+      else if (rep.isEmpty) other
+      else (this /: other.iterator)(_ + _)
+
+    override def hashCode: Int = rep.hashCode
+    override def equals(that: Any): Boolean =
+      that match {
+        case other: Exports => rep == other.rep
+        case _ => false
+      }
+    override def toString: String = iterator.mkString("Exports(", ", ", ")")
+  }
+
+
+  /* markups */
 
   object Markup_Index
   {
@@ -175,6 +207,9 @@
     def merge_results(states: List[State]): Results =
       Results.merge(states.map(_.results))
 
+    def merge_exports(states: List[State]): Exports =
+      Exports.merge(states.map(_.exports))
+
     def merge_markups(states: List[State]): Markups =
       Markups.merge(states.map(_.markups))
 
@@ -183,7 +218,8 @@
       Markup_Tree.merge(states.map(_.markup(index)), range, elements)
 
     def merge(command: Command, states: List[State]): State =
-      State(command, states.flatMap(_.status), merge_results(states), merge_markups(states))
+      State(command, states.flatMap(_.status), merge_results(states),
+        merge_exports(states), merge_markups(states))
 
 
     /* XML data representation */
@@ -213,7 +249,7 @@
       val blobs_info: Blobs_Info =
         (blobs_names.map(name => Exn.Res((node_name(name), None)): Blob), blobs_index)
       val command = Command(id, node_name(node), blobs_info, span)
-      State(command, status, results, markups)
+      State(command, status, results, Exports.empty, markups)
     }
   }
 
@@ -221,6 +257,7 @@
     command: Command,
     status: List[Markup] = Nil,
     results: Results = Results.empty,
+    exports: Exports = Exports.empty,
     markups: Markups = Markups.empty)
   {
     lazy val consolidated: Boolean =
@@ -245,7 +282,7 @@
     {
       val markups1 = markups.redirect(other_command.id)
       if (markups1.is_empty) None
-      else Some(new State(other_command, Nil, Results.empty, markups1))
+      else Some(new State(other_command, markups = markups1))
     }
 
     private def add_status(st: Markup): State =
@@ -254,6 +291,9 @@
     private def add_result(entry: Results.Entry): State =
       copy(results = results + entry)
 
+    def add_export(entry: Exports.Entry): State =
+      copy(exports = exports + entry)
+
     private def add_markup(
       status: Boolean, chunk_name: Symbol.Text_Chunk.Name, m: Text.Markup): State =
     {
@@ -342,7 +382,7 @@
               Output.warning("Ignored message without serial number: " + message)
               this
           }
-    }
+      }
   }
 
 

--- a/src/Pure/PIDE/document.scala	Sun May 06 23:59:14 2018 +0100
+++ b/src/Pure/PIDE/document.scala	Mon May 07 17:11:01 2018 +0200
@@ -721,6 +721,22 @@
       }
     }
 
+    def add_export(id: Document_ID.Generic, entry: Command.Exports.Entry): (Command.State, State) =
+    {
+      execs.get(id) match {
+        case Some(st) =>
+          val new_st = st.add_export(entry)
+          (new_st, copy(execs = execs + (id -> new_st)))
+        case None =>
+          commands.get(id) match {
+            case Some(st) =>
+              val new_st = st.add_export(entry)
+              (new_st, copy(commands = commands + (id -> new_st)))
+            case None => fail
+          }
+      }
+    }
+
     def assign(id: Document_ID.Version, update: Assign_Update): (List[Command], State) =
     {
       val version = the_version(id)

--- a/src/Pure/PIDE/markup.ML	Sun May 06 23:59:14 2018 +0100
+++ b/src/Pure/PIDE/markup.ML	Mon May 07 17:11:01 2018 +0200
@@ -203,7 +203,8 @@
   val command_timing: Properties.entry
   val theory_timing: Properties.entry
   val exportN: string
-  type export_args = {id: string option, theory_name: string, name: string, compress: bool}
+  type export_args =
+    {id: string option, serial: serial, theory_name: string, name: string, compress: bool}
   val export: export_args -> Properties.T
   val loading_theory: string -> Properties.T
   val dest_loading_theory: Properties.T -> string option
@@ -642,9 +643,10 @@
 val theory_timing = (functionN, "theory_timing");
 
 val exportN = "export";
-type export_args = {id: string option, theory_name: string, name: string, compress: bool}
-fun export ({id, theory_name, name, compress}: export_args) =
-  [(functionN, exportN), (idN, the_default "" id),
+type export_args =
+  {id: string option, serial: serial, theory_name: string, name: string, compress: bool}
+fun export ({id, serial, theory_name, name, compress}: export_args) =
+  [(functionN, exportN), (idN, the_default "" id), (serialN, Value.print_int serial),
     ("theory_name", theory_name), (nameN, name), ("compress", Value.print_bool compress)];
 
 fun loading_theory name = [("function", "loading_theory"), ("name", name)];

--- a/src/Pure/PIDE/markup.scala	Sun May 06 23:59:14 2018 +0100
+++ b/src/Pure/PIDE/markup.scala	Mon May 07 17:11:01 2018 +0200
@@ -571,7 +571,8 @@
   val EXPORT = "export"
   object Export
   {
-    sealed case class Args(id: Option[String], theory_name: String, name: String, compress: Boolean)
+    sealed case class Args(
+      id: Option[String], serial: Long, theory_name: String, name: String, compress: Boolean)
 
     val THEORY_NAME = "theory_name"
     val COMPRESS = "compress"
@@ -579,16 +580,26 @@
     def dest_inline(props: Properties.T): Option[(Args, Bytes)] =
       props match {
         case
-          List((THEORY_NAME, theory_name), (NAME, name), (COMPRESS, Value.Boolean(compress)),
-            (EXPORT, hex)) => Some((Args(None, theory_name, name, compress), Bytes.hex(hex)))
+          List(
+            (SERIAL, Value.Long(serial)),
+            (THEORY_NAME, theory_name),
+            (NAME, name),
+            (COMPRESS, Value.Boolean(compress)),
+            (EXPORT, hex)) =>
+          Some((Args(None, serial, theory_name, name, 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, name), (COMPRESS, Value.Boolean(compress))) =>
-            Some(Args(proper_string(id), theory_name, name, compress))
+        case List(
+            (FUNCTION, EXPORT),
+            (ID, id),
+            (SERIAL, Value.Long(serial)),
+            (THEORY_NAME, theory_name),
+            (NAME, name),
+            (COMPRESS, Value.Boolean(compress))) =>
+          Some(Args(proper_string(id), serial, theory_name, name, compress))
         case _ => None
       }
   }

--- a/src/Pure/PIDE/session.scala	Sun May 06 23:59:14 2018 +0100
+++ b/src/Pure/PIDE/session.scala	Mon May 07 17:11:01 2018 +0200
@@ -191,6 +191,7 @@
   private case object Stop
   private case class Cancel_Exec(exec_id: Document_ID.Exec)
   private case class Protocol_Command(name: String, args: List[String])
+  private case class Add_Export(args: Markup.Export.Args, bytes: Bytes, output: Prover.Output)
   private case class Update_Options(options: Options)
   private case object Consolidate_Execution
   private case object Prune_History
@@ -400,25 +401,26 @@
 
     /* prover output */
 
+    def bad_output(output: Prover.Output)
+    {
+      if (verbose)
+        Output.warning("Ignoring bad prover output: " + output.message.toString)
+    }
+
+    def change_command(f: Document.State => (Command.State, Document.State), output: Prover.Output)
+    {
+      try {
+        val st = global_state.change_result(f)
+        change_buffer.invoke(false, List(st.command))
+      }
+      catch { case _: Document.State.Fail => bad_output(output) }
+    }
+
     def handle_output(output: Prover.Output)
     //{{{
     {
-      def bad_output()
-      {
-        if (verbose)
-          Output.warning("Ignoring bad prover output: " + output.message.toString)
-      }
-
-      def accumulate(state_id: Document_ID.Generic, message: XML.Elem)
-      {
-        try {
-          val st = global_state.change_result(_.accumulate(state_id, message, xml_cache))
-          change_buffer.invoke(false, List(st.command))
-        }
-        catch {
-          case _: Document.State.Fail => bad_output()
-        }
-      }
+      def accumulate(state_id: Document_ID.Generic, message: XML.Elem): Unit =
+        change_command(_.accumulate(state_id, message, xml_cache), output)
 
       output match {
         case msg: Prover.Protocol_Output =>
@@ -435,8 +437,12 @@
               case Protocol.Theory_Timing(_, _) =>
                 // FIXME
 
-              case Markup.Export(_) =>
-                // FIXME
+              case Markup.Export(args)
+              if args.id.isDefined && Value.Long.unapply(args.id.get).isDefined =>
+                if (args.compress) {
+                  Future.fork { manager.send(Add_Export(args, msg.bytes.compress(), output)) }
+                }
+                else manager.send(Add_Export(args, msg.bytes, output))
 
               case Markup.Assign_Update =>
                 msg.text match {
@@ -446,8 +452,8 @@
                       change_buffer.invoke(true, cmds)
                       manager.send(Session.Change_Flush)
                     }
-                    catch { case _: Document.State.Fail => bad_output() }
-                  case _ => bad_output()
+                    catch { case _: Document.State.Fail => bad_output(output) }
+                  case _ => bad_output(output)
                 }
                 delay_prune.invoke()
 
@@ -458,8 +464,8 @@
                       global_state.change(_.removed_versions(removed))
                       manager.send(Session.Change_Flush)
                     }
-                    catch { case _: Document.State.Fail => bad_output() }
-                  case _ => bad_output()
+                    catch { case _: Document.State.Fail => bad_output(output) }
+                  case _ => bad_output(output)
                 }
 
               case Markup.ML_Statistics(props) =>
@@ -468,7 +474,7 @@
               case Markup.Task_Statistics(props) =>
                 // FIXME
 
-              case _ => bad_output()
+              case _ => bad_output(output)
             }
           }
         case _ =>
@@ -556,6 +562,11 @@
           case Protocol_Command(name, args) if prover.defined =>
             prover.get.protocol_command(name, args:_*)
 
+          case Add_Export(args, bytes, output) =>
+            val id = Value.Long.parse(args.id.get)
+            val entry = (args.serial, Export.make_entry("", args, bytes))
+            change_command(_.add_export(id, entry), output)
+
           case change: Session.Change if prover.defined =>
             val state = global_state.value
             if (!state.removing_versions && state.is_assigned(change.previous))

--- a/src/Pure/Thy/export.ML	Sun May 06 23:59:14 2018 +0100
+++ b/src/Pure/Thy/export.ML	Mon May 07 17:11:01 2018 +0200
@@ -16,6 +16,7 @@
 fun gen_export compress thy name output =
   (Output.try_protocol_message o Markup.export)
    {id = Position.get_id (Position.thread_data ()),
+    serial = serial (),
     theory_name = Context.theory_long_name thy,
     name = name,
     compress = compress} [output];

--- a/src/Pure/Thy/export.scala	Sun May 06 23:59:14 2018 +0100
+++ b/src/Pure/Thy/export.scala	Mon May 07 17:11:01 2018 +0200
@@ -58,6 +58,12 @@
     }
   }
 
+  def make_entry(session_name: String, args: Markup.Export.Args, body: Bytes): Entry =
+  {
+    val bytes = if (args.compress) body.compress() else body
+    Entry(session_name, args.theory_name, args.name, args.compress, bytes)
+  }
+
   def read_entry(db: SQL.Database, session_name: String, theory_name: String, name: String): Entry =
   {
     val select =
@@ -104,9 +110,9 @@
     {
       consumer.send(
         if (args.compress)
-          Future.fork(Entry(session_name, args.theory_name, args.name, true, body.compress()))
+          Future.fork(make_entry(session_name, args, body))
         else
-          Future.value(Entry(session_name, args.theory_name, args.name, false, body)))
+          Future.value(make_entry(session_name, args, body)))
     }
 
     def shutdown(close: Boolean = false): List[String] =