src/Pure/Thy/export_theory.scala
changeset 68997 4278947ba336
parent 68864 1dacce27bc25
child 69003 a015f1d3ba0c
     1.1 --- a/src/Pure/Thy/export_theory.scala	Sat Sep 15 22:33:48 2018 +0200
     1.2 +++ b/src/Pure/Thy/export_theory.scala	Sat Sep 15 23:35:46 2018 +0200
     1.3 @@ -165,12 +165,12 @@
     1.4    }
     1.5  
     1.6    sealed case class Entity(
     1.7 -    kind: Kind.Value, name: String, pos: Position.T, id: Option[Long], serial: Long)
     1.8 +    kind: Kind.Value, name: String, xname: String, pos: Position.T, id: Option[Long], serial: Long)
     1.9    {
    1.10      override def toString: String = kind.toString + " " + quote(name)
    1.11  
    1.12      def cache(cache: Term.Cache): Entity =
    1.13 -      Entity(kind, cache.string(name), cache.position(pos), id, serial)
    1.14 +      Entity(kind, cache.string(name), cache.string(xname), cache.position(pos), id, serial)
    1.15    }
    1.16  
    1.17    def decode_entity(kind: Kind.Value, tree: XML.Tree): (Entity, XML.Body) =
    1.18 @@ -180,10 +180,11 @@
    1.19      tree match {
    1.20        case XML.Elem(Markup(Markup.ENTITY, props), body) =>
    1.21          val name = Markup.Name.unapply(props) getOrElse err()
    1.22 +        val xname = Markup.XName.unapply(props) getOrElse err()
    1.23          val pos = props.filter({ case (a, _) => Markup.POSITION_PROPERTIES(a) && a != Markup.ID })
    1.24          val id = Position.Id.unapply(props)
    1.25          val serial = Markup.Serial.unapply(props) getOrElse err()
    1.26 -        (Entity(kind, name, pos, id, serial), body)
    1.27 +        (Entity(kind, name, xname, pos, id, serial), body)
    1.28        case _ => err()
    1.29      }
    1.30    }