# HG changeset patch
# User wenzelm
# Date 1535462728 -7200
# Node ID 2e59da92263029ddc4f184ab2c6868d84143f5fa
# Parent  9b9fc9ea9dd1624bd95a6748b520eee1934b57e7
more robust: Pure entities may lack id;

diff -r 9b9fc9ea9dd1 -r 2e59da922630 src/Pure/Thy/export_theory.scala
--- a/src/Pure/Thy/export_theory.scala	Tue Aug 28 12:42:57 2018 +0200
+++ b/src/Pure/Thy/export_theory.scala	Tue Aug 28 15:25:28 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()