# HG changeset patch
# User wenzelm
# Date 1526235873 -7200
# Node ID 0f14cf9c632fe17563a7eb3f330951a8315c5c63
# Parent  13162bb3a6775475304e40c2440ca9bf998f4b7f
more concise information;

diff -r 13162bb3a677 -r 0f14cf9c632f src/Pure/General/position.ML
--- a/src/Pure/General/position.ML	Sun May 13 20:04:59 2018 +0200
+++ b/src/Pure/General/position.ML	Sun May 13 20:24:33 2018 +0200
@@ -32,6 +32,7 @@
   val parse_id: T -> int option
   val of_properties: Properties.T -> T
   val properties_of: T -> Properties.T
+  val offset_properties_of: T -> Properties.T
   val def_properties_of: T -> Properties.T
   val entity_properties_of: bool -> serial -> T -> Properties.T
   val default_properties: T -> Properties.T -> Properties.T
@@ -161,6 +162,9 @@
 fun properties_of (Pos ((i, j, k), props)) =
   value Markup.lineN i @ value Markup.offsetN j @ value Markup.end_offsetN k @ props;
 
+fun offset_properties_of (Pos ((_, j, k), _)) =
+  value Markup.offsetN j @ value Markup.end_offsetN k;
+
 val def_properties_of = properties_of #> map (fn (x, y) => ("def_" ^ x, y));
 
 fun entity_properties_of def serial pos =
diff -r 13162bb3a677 -r 0f14cf9c632f src/Pure/Thy/export_theory.ML
--- a/src/Pure/Thy/export_theory.ML	Sun May 13 20:04:59 2018 +0200
+++ b/src/Pure/Thy/export_theory.ML	Sun May 13 20:24:33 2018 +0200
@@ -16,10 +16,9 @@
 
 fun entity_markup space name =
   let
-    val kind = Name_Space.kind_of space;
     val {serial, pos, ...} = Name_Space.the_entry space name;
-    val props = Markup.serial_properties serial @ Position.properties_of pos;
-  in Markup.properties props (Markup.entity kind name) end;
+    val props = Markup.serial_properties serial @ Position.offset_properties_of pos;
+  in (Markup.entityN, (Markup.nameN, name) :: props) end;
 
 fun export_decls export_decl parents space decls =
   (decls, []) |-> fold (fn (name, decl) =>
diff -r 13162bb3a677 -r 0f14cf9c632f src/Pure/Thy/export_theory.scala
--- a/src/Pure/Thy/export_theory.scala	Sun May 13 20:04:59 2018 +0200
+++ b/src/Pure/Thy/export_theory.scala	Sun May 13 20:24:33 2018 +0200
@@ -11,7 +11,7 @@
 {
   /* entities */
 
-  sealed case class Entity(name: String, kind: String, serial: Long, pos: Position.T)
+  sealed case class Entity(name: String, serial: Long, pos: Position.T)
   {
     override def toString: String = name
   }
@@ -23,10 +23,9 @@
     tree match {
       case XML.Elem(Markup(Markup.ENTITY, props), body) =>
         val name = Markup.Name.unapply(props) getOrElse err()
-        val kind = Markup.Kind.unapply(props) getOrElse err()
         val serial = Markup.Serial.unapply(props) getOrElse err()
         val pos = props.filter({ case (a, _) => Markup.POSITION_PROPERTIES(a) })
-        (Entity(name, kind, serial, pos), body)
+        (Entity(name, serial, pos), body)
       case _ => err()
     }
   }