src/Pure/Thy/export_theory.scala
changeset 68835 2e59da922630
parent 68830 44ec6fdaacf8
child 68862 47e9912c53c3
     1.1 --- a/src/Pure/Thy/export_theory.scala	Tue Aug 28 12:42:57 2018 +0200
     1.2 +++ b/src/Pure/Thy/export_theory.scala	Tue Aug 28 15:25:28 2018 +0200
     1.3 @@ -156,7 +156,8 @@
     1.4      val CLASS = Value("class")
     1.5    }
     1.6  
     1.7 -  sealed case class Entity(kind: Kind.Value, name: String, pos: Position.T, id: Long, serial: Long)
     1.8 +  sealed case class Entity(
     1.9 +    kind: Kind.Value, name: String, pos: Position.T, id: Option[Long], serial: Long)
    1.10    {
    1.11      override def toString: String = kind.toString + " " + quote(name)
    1.12  
    1.13 @@ -172,7 +173,7 @@
    1.14        case XML.Elem(Markup(Markup.ENTITY, props), body) =>
    1.15          val name = Markup.Name.unapply(props) getOrElse err()
    1.16          val pos = props.filter({ case (a, _) => Markup.POSITION_PROPERTIES(a) && a != Markup.ID })
    1.17 -        val id = Position.Id.unapply(props) getOrElse err()
    1.18 +        val id = Position.Id.unapply(props)
    1.19          val serial = Markup.Serial.unapply(props) getOrElse err()
    1.20          (Entity(kind, name, pos, id, serial), body)
    1.21        case _ => err()