retain original id, which is command_id/exec_id for PIDE;
authorwenzelm
Tue Aug 28 12:07:30 2018 +0200 (10 months ago)
changeset 6883044ec6fdaacf8
parent 68829 1a4fa494a4a8
child 68831 a6c69599ab99
retain original id, which is command_id/exec_id for PIDE;
tuned;
src/Pure/Thy/export_theory.ML
src/Pure/Thy/export_theory.scala
     1.1 --- a/src/Pure/Thy/export_theory.ML	Tue Aug 28 11:40:11 2018 +0200
     1.2 +++ b/src/Pure/Thy/export_theory.ML	Tue Aug 28 12:07:30 2018 +0200
     1.3 @@ -66,8 +66,9 @@
     1.4        let
     1.5          val {serial, pos, ...} = Name_Space.the_entry space name;
     1.6          val props =
     1.7 -          Markup.serial_properties serial @
     1.8 -          Position.offset_properties_of (adjust_pos pos);
     1.9 +          Position.offset_properties_of (adjust_pos pos) @
    1.10 +          Position.id_properties_of pos @
    1.11 +          Markup.serial_properties serial;
    1.12        in (Markup.entityN, (Markup.nameN, name) :: props) end;
    1.13  
    1.14      fun export_entities export_name export get_space decls =
     2.1 --- a/src/Pure/Thy/export_theory.scala	Tue Aug 28 11:40:11 2018 +0200
     2.2 +++ b/src/Pure/Thy/export_theory.scala	Tue Aug 28 12:07:30 2018 +0200
     2.3 @@ -156,12 +156,12 @@
     2.4      val CLASS = Value("class")
     2.5    }
     2.6  
     2.7 -  sealed case class Entity(kind: Kind.Value, name: String, serial: Long, pos: Position.T)
     2.8 +  sealed case class Entity(kind: Kind.Value, name: String, pos: Position.T, id: Long, serial: Long)
     2.9    {
    2.10      override def toString: String = kind.toString + " " + quote(name)
    2.11  
    2.12      def cache(cache: Term.Cache): Entity =
    2.13 -      Entity(kind, cache.string(name), serial, cache.position(pos))
    2.14 +      Entity(kind, cache.string(name), cache.position(pos), id, serial)
    2.15    }
    2.16  
    2.17    def decode_entity(kind: Kind.Value, tree: XML.Tree): (Entity, XML.Body) =
    2.18 @@ -171,9 +171,10 @@
    2.19      tree match {
    2.20        case XML.Elem(Markup(Markup.ENTITY, props), body) =>
    2.21          val name = Markup.Name.unapply(props) getOrElse err()
    2.22 +        val pos = props.filter({ case (a, _) => Markup.POSITION_PROPERTIES(a) && a != Markup.ID })
    2.23 +        val id = Position.Id.unapply(props) getOrElse err()
    2.24          val serial = Markup.Serial.unapply(props) getOrElse err()
    2.25 -        val pos = props.filter({ case (a, _) => Markup.POSITION_PROPERTIES(a) })
    2.26 -        (Entity(kind, name, serial, pos), body)
    2.27 +        (Entity(kind, name, pos, id, serial), body)
    2.28        case _ => err()
    2.29      }
    2.30    }