merged

--- a/src/Pure/PIDE/document.scala	Tue Aug 28 13:45:40 2018 +0100
+++ b/src/Pure/PIDE/document.scala	Tue Aug 28 21:08:42 2018 +0200
@@ -560,6 +560,8 @@
 
     def command_results(range: Text.Range): Command.Results
     def command_results(command: Command): Command.Results
+
+    def command_id_map: Map[Document_ID.Generic, Command]
   }
 
 
@@ -860,6 +862,17 @@
         removing_versions = false)
     }
 
+    def command_id_map(version: Version, commands: Iterable[Command])
+      : Map[Document_ID.Generic, Command] =
+    {
+      require(is_assigned(version))
+      val assignment = the_assignment(version).check_finished
+      (for {
+        command <- commands.iterator
+        id <- (command.id :: assignment.command_execs.getOrElse(command.id, Nil)).iterator
+      } yield (id -> command)).toMap
+    }
+
     def command_state_eval(version: Version, command: Command): Option[Command.State] =
     {
       require(is_assigned(version))
@@ -1148,6 +1161,12 @@
           state.command_results(version, command)
 
 
+        /* command ids: static and dynamic */
+
+        def command_id_map: Map[Document_ID.Generic, Command] =
+          state.command_id_map(version, version.nodes(node_name).commands)
+
+
         /* output */
 
         override def toString: String =

--- a/src/Pure/Thy/export_theory.scala	Tue Aug 28 13:45:40 2018 +0100
+++ b/src/Pure/Thy/export_theory.scala	Tue Aug 28 21:08:42 2018 +0200
@@ -156,7 +156,8 @@
     val CLASS = Value("class")
   }
 
-  sealed case class Entity(kind: Kind.Value, name: String, pos: Position.T, id: Long, serial: Long)
+  sealed case class Entity(
+    kind: Kind.Value, name: String, pos: Position.T, id: Option[Long], serial: Long)
   {
     override def toString: String = kind.toString + " " + quote(name)
 
@@ -172,7 +173,7 @@
       case XML.Elem(Markup(Markup.ENTITY, props), body) =>
         val name = Markup.Name.unapply(props) getOrElse err()
         val pos = props.filter({ case (a, _) => Markup.POSITION_PROPERTIES(a) && a != Markup.ID })
-        val id = Position.Id.unapply(props) getOrElse err()
+        val id = Position.Id.unapply(props)
         val serial = Markup.Serial.unapply(props) getOrElse err()
         (Entity(kind, name, pos, id, serial), body)
       case _ => err()