diff -r 5f3cffe16311 -r 0699a0bacc50 src/Pure/PIDE/document.scala
--- 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)