# HG changeset patch
# User wenzelm
# Date 1535450850 -7200
# Node ID 44ec6fdaacf8b8eb1b44a5b1da58c48083a09ba0
# Parent  1a4fa494a4a8b07a2b091920f9f7fdfdc81a0d97
retain original id, which is command_id/exec_id for PIDE;
tuned;

diff -r 1a4fa494a4a8 -r 44ec6fdaacf8 src/Pure/Thy/export_theory.ML
--- a/src/Pure/Thy/export_theory.ML	Tue Aug 28 11:40:11 2018 +0200
+++ b/src/Pure/Thy/export_theory.ML	Tue Aug 28 12:07:30 2018 +0200
@@ -66,8 +66,9 @@
       let
         val {serial, pos, ...} = Name_Space.the_entry space name;
         val props =
-          Markup.serial_properties serial @
-          Position.offset_properties_of (adjust_pos pos);
+          Position.offset_properties_of (adjust_pos pos) @
+          Position.id_properties_of pos @
+          Markup.serial_properties serial;
       in (Markup.entityN, (Markup.nameN, name) :: props) end;
 
     fun export_entities export_name export get_space decls =
diff -r 1a4fa494a4a8 -r 44ec6fdaacf8 src/Pure/Thy/export_theory.scala
--- a/src/Pure/Thy/export_theory.scala	Tue Aug 28 11:40:11 2018 +0200
+++ b/src/Pure/Thy/export_theory.scala	Tue Aug 28 12:07:30 2018 +0200
@@ -156,12 +156,12 @@
     val CLASS = Value("class")
   }
 
-  sealed case class Entity(kind: Kind.Value, name: String, serial: Long, pos: Position.T)
+  sealed case class Entity(kind: Kind.Value, name: String, pos: Position.T, id: Long, serial: Long)
   {
     override def toString: String = kind.toString + " " + quote(name)
 
     def cache(cache: Term.Cache): Entity =
-      Entity(kind, cache.string(name), serial, cache.position(pos))
+      Entity(kind, cache.string(name), cache.position(pos), id, serial)
   }
 
   def decode_entity(kind: Kind.Value, tree: XML.Tree): (Entity, XML.Body) =
@@ -171,9 +171,10 @@
     tree match {
       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 serial = Markup.Serial.unapply(props) getOrElse err()
-        val pos = props.filter({ case (a, _) => Markup.POSITION_PROPERTIES(a) })
-        (Entity(kind, name, serial, pos), body)
+        (Entity(kind, name, pos, id, serial), body)
       case _ => err()
     }
   }