# HG changeset patch
# User wenzelm
# Date 1537047346 -7200
# Node ID 4278947ba336007da9df7e65aea87bab43215ac4
# Parent  5f333f88d2c1ffff46f2447283329df28764d146
more exports;

diff -r 5f333f88d2c1 -r 4278947ba336 src/Pure/PIDE/markup.ML
--- a/src/Pure/PIDE/markup.ML	Sat Sep 15 22:33:48 2018 +0200
+++ b/src/Pure/PIDE/markup.ML	Sat Sep 15 23:35:46 2018 +0200
@@ -10,8 +10,8 @@
   val empty: T
   val is_empty: T -> bool
   val properties: Properties.T -> T -> T
-  val nameN: string
-  val name: string -> T -> T
+  val nameN: string val name: string -> T -> T
+  val xnameN: string val xname: string -> T -> T
   val kindN: string
   val serialN: string
   val serial_properties: int -> Properties.T
@@ -260,6 +260,9 @@
 val nameN = "name";
 fun name a = properties [(nameN, a)];
 
+val xnameN = "xname";
+fun xname a = properties [(xnameN, a)];
+
 val kindN = "kind";
 
 val serialN = "serial";
diff -r 5f333f88d2c1 -r 4278947ba336 src/Pure/PIDE/markup.scala
--- a/src/Pure/PIDE/markup.scala	Sat Sep 15 22:33:48 2018 +0200
+++ b/src/Pure/PIDE/markup.scala	Sat Sep 15 23:35:46 2018 +0200
@@ -40,6 +40,9 @@
   val NAME = "name"
   val Name = new Properties.String(NAME)
 
+  val XNAME = "xname"
+  val XName = new Properties.String(XNAME)
+
   val KIND = "kind"
   val Kind = new Properties.String(KIND)
 
diff -r 5f333f88d2c1 -r 4278947ba336 src/Pure/Thy/export_theory.ML
--- a/src/Pure/Thy/export_theory.ML	Sat Sep 15 22:33:48 2018 +0200
+++ b/src/Pure/Thy/export_theory.ML	Sat Sep 15 23:35:46 2018 +0200
@@ -52,17 +52,20 @@
     val parents = Theory.parents_of thy;
     val rep_tsig = Type.rep_tsig (Sign.tsig_of thy);
 
+    val ctxt = Proof_Context.init_global thy;
+
 
     (* entities *)
 
     fun entity_markup space name =
       let
+        val xname = Name_Space.extern_shortest ctxt space name;
         val {serial, pos, ...} = Name_Space.the_entry space name;
         val props =
           Position.offset_properties_of (adjust_pos pos) @
           Position.id_properties_of pos @
           Markup.serial_properties serial;
-      in (Markup.entityN, (Markup.nameN, name) :: props) end;
+      in (Markup.entityN, (Markup.nameN, name) :: (Markup.xnameN, xname) :: props) end;
 
     fun export_entities export_name export get_space decls =
       let val elems =
diff -r 5f333f88d2c1 -r 4278947ba336 src/Pure/Thy/export_theory.scala
--- a/src/Pure/Thy/export_theory.scala	Sat Sep 15 22:33:48 2018 +0200
+++ b/src/Pure/Thy/export_theory.scala	Sat Sep 15 23:35:46 2018 +0200
@@ -165,12 +165,12 @@
   }
 
   sealed case class Entity(
-    kind: Kind.Value, name: String, pos: Position.T, id: Option[Long], serial: Long)
+    kind: Kind.Value, name: String, xname: String, pos: Position.T, id: Option[Long], serial: Long)
   {
     override def toString: String = kind.toString + " " + quote(name)
 
     def cache(cache: Term.Cache): Entity =
-      Entity(kind, cache.string(name), cache.position(pos), id, serial)
+      Entity(kind, cache.string(name), cache.string(xname), cache.position(pos), id, serial)
   }
 
   def decode_entity(kind: Kind.Value, tree: XML.Tree): (Entity, XML.Body) =
@@ -180,10 +180,11 @@
     tree match {
       case XML.Elem(Markup(Markup.ENTITY, props), body) =>
         val name = Markup.Name.unapply(props) getOrElse err()
+        val xname = Markup.XName.unapply(props) getOrElse err()
         val pos = props.filter({ case (a, _) => Markup.POSITION_PROPERTIES(a) && a != Markup.ID })
         val id = Position.Id.unapply(props)
         val serial = Markup.Serial.unapply(props) getOrElse err()
-        (Entity(kind, name, pos, id, serial), body)
+        (Entity(kind, name, xname, pos, id, serial), body)
       case _ => err()
     }
   }