more exports;
authorwenzelm
Sat Sep 15 23:35:46 2018 +0200 (3 days ago)
changeset 689974278947ba336
parent 68996 5f333f88d2c1
child 68998 818898556504
child 69000 7cb3ddd60fd6
more exports;
src/Pure/PIDE/markup.ML
src/Pure/PIDE/markup.scala
src/Pure/Thy/export_theory.ML
src/Pure/Thy/export_theory.scala
     1.1 --- a/src/Pure/PIDE/markup.ML	Sat Sep 15 22:33:48 2018 +0200
     1.2 +++ b/src/Pure/PIDE/markup.ML	Sat Sep 15 23:35:46 2018 +0200
     1.3 @@ -10,8 +10,8 @@
     1.4    val empty: T
     1.5    val is_empty: T -> bool
     1.6    val properties: Properties.T -> T -> T
     1.7 -  val nameN: string
     1.8 -  val name: string -> T -> T
     1.9 +  val nameN: string val name: string -> T -> T
    1.10 +  val xnameN: string val xname: string -> T -> T
    1.11    val kindN: string
    1.12    val serialN: string
    1.13    val serial_properties: int -> Properties.T
    1.14 @@ -260,6 +260,9 @@
    1.15  val nameN = "name";
    1.16  fun name a = properties [(nameN, a)];
    1.17  
    1.18 +val xnameN = "xname";
    1.19 +fun xname a = properties [(xnameN, a)];
    1.20 +
    1.21  val kindN = "kind";
    1.22  
    1.23  val serialN = "serial";
     2.1 --- a/src/Pure/PIDE/markup.scala	Sat Sep 15 22:33:48 2018 +0200
     2.2 +++ b/src/Pure/PIDE/markup.scala	Sat Sep 15 23:35:46 2018 +0200
     2.3 @@ -40,6 +40,9 @@
     2.4    val NAME = "name"
     2.5    val Name = new Properties.String(NAME)
     2.6  
     2.7 +  val XNAME = "xname"
     2.8 +  val XName = new Properties.String(XNAME)
     2.9 +
    2.10    val KIND = "kind"
    2.11    val Kind = new Properties.String(KIND)
    2.12  
     3.1 --- a/src/Pure/Thy/export_theory.ML	Sat Sep 15 22:33:48 2018 +0200
     3.2 +++ b/src/Pure/Thy/export_theory.ML	Sat Sep 15 23:35:46 2018 +0200
     3.3 @@ -52,17 +52,20 @@
     3.4      val parents = Theory.parents_of thy;
     3.5      val rep_tsig = Type.rep_tsig (Sign.tsig_of thy);
     3.6  
     3.7 +    val ctxt = Proof_Context.init_global thy;
     3.8 +
     3.9  
    3.10      (* entities *)
    3.11  
    3.12      fun entity_markup space name =
    3.13        let
    3.14 +        val xname = Name_Space.extern_shortest ctxt space name;
    3.15          val {serial, pos, ...} = Name_Space.the_entry space name;
    3.16          val props =
    3.17            Position.offset_properties_of (adjust_pos pos) @
    3.18            Position.id_properties_of pos @
    3.19            Markup.serial_properties serial;
    3.20 -      in (Markup.entityN, (Markup.nameN, name) :: props) end;
    3.21 +      in (Markup.entityN, (Markup.nameN, name) :: (Markup.xnameN, xname) :: props) end;
    3.22  
    3.23      fun export_entities export_name export get_space decls =
    3.24        let val elems =
     4.1 --- a/src/Pure/Thy/export_theory.scala	Sat Sep 15 22:33:48 2018 +0200
     4.2 +++ b/src/Pure/Thy/export_theory.scala	Sat Sep 15 23:35:46 2018 +0200
     4.3 @@ -165,12 +165,12 @@
     4.4    }
     4.5  
     4.6    sealed case class Entity(
     4.7 -    kind: Kind.Value, name: String, pos: Position.T, id: Option[Long], serial: Long)
     4.8 +    kind: Kind.Value, name: String, xname: String, pos: Position.T, id: Option[Long], serial: Long)
     4.9    {
    4.10      override def toString: String = kind.toString + " " + quote(name)
    4.11  
    4.12      def cache(cache: Term.Cache): Entity =
    4.13 -      Entity(kind, cache.string(name), cache.position(pos), id, serial)
    4.14 +      Entity(kind, cache.string(name), cache.string(xname), cache.position(pos), id, serial)
    4.15    }
    4.16  
    4.17    def decode_entity(kind: Kind.Value, tree: XML.Tree): (Entity, XML.Body) =
    4.18 @@ -180,10 +180,11 @@
    4.19      tree match {
    4.20        case XML.Elem(Markup(Markup.ENTITY, props), body) =>
    4.21          val name = Markup.Name.unapply(props) getOrElse err()
    4.22 +        val xname = Markup.XName.unapply(props) getOrElse err()
    4.23          val pos = props.filter({ case (a, _) => Markup.POSITION_PROPERTIES(a) && a != Markup.ID })
    4.24          val id = Position.Id.unapply(props)
    4.25          val serial = Markup.Serial.unapply(props) getOrElse err()
    4.26 -        (Entity(kind, name, pos, id, serial), body)
    4.27 +        (Entity(kind, name, xname, pos, id, serial), body)
    4.28        case _ => err()
    4.29      }
    4.30    }