more concise information;
authorwenzelm
Sun May 13 20:24:33 2018 +0200 (12 months ago)
changeset 681720f14cf9c632f
parent 68171 13162bb3a677
child 68173 7ed88a534bb6
more concise information;
src/Pure/General/position.ML
src/Pure/Thy/export_theory.ML
src/Pure/Thy/export_theory.scala
     1.1 --- a/src/Pure/General/position.ML	Sun May 13 20:04:59 2018 +0200
     1.2 +++ b/src/Pure/General/position.ML	Sun May 13 20:24:33 2018 +0200
     1.3 @@ -32,6 +32,7 @@
     1.4    val parse_id: T -> int option
     1.5    val of_properties: Properties.T -> T
     1.6    val properties_of: T -> Properties.T
     1.7 +  val offset_properties_of: T -> Properties.T
     1.8    val def_properties_of: T -> Properties.T
     1.9    val entity_properties_of: bool -> serial -> T -> Properties.T
    1.10    val default_properties: T -> Properties.T -> Properties.T
    1.11 @@ -161,6 +162,9 @@
    1.12  fun properties_of (Pos ((i, j, k), props)) =
    1.13    value Markup.lineN i @ value Markup.offsetN j @ value Markup.end_offsetN k @ props;
    1.14  
    1.15 +fun offset_properties_of (Pos ((_, j, k), _)) =
    1.16 +  value Markup.offsetN j @ value Markup.end_offsetN k;
    1.17 +
    1.18  val def_properties_of = properties_of #> map (fn (x, y) => ("def_" ^ x, y));
    1.19  
    1.20  fun entity_properties_of def serial pos =
     2.1 --- a/src/Pure/Thy/export_theory.ML	Sun May 13 20:04:59 2018 +0200
     2.2 +++ b/src/Pure/Thy/export_theory.ML	Sun May 13 20:24:33 2018 +0200
     2.3 @@ -16,10 +16,9 @@
     2.4  
     2.5  fun entity_markup space name =
     2.6    let
     2.7 -    val kind = Name_Space.kind_of space;
     2.8      val {serial, pos, ...} = Name_Space.the_entry space name;
     2.9 -    val props = Markup.serial_properties serial @ Position.properties_of pos;
    2.10 -  in Markup.properties props (Markup.entity kind name) end;
    2.11 +    val props = Markup.serial_properties serial @ Position.offset_properties_of pos;
    2.12 +  in (Markup.entityN, (Markup.nameN, name) :: props) end;
    2.13  
    2.14  fun export_decls export_decl parents space decls =
    2.15    (decls, []) |-> fold (fn (name, decl) =>
     3.1 --- a/src/Pure/Thy/export_theory.scala	Sun May 13 20:04:59 2018 +0200
     3.2 +++ b/src/Pure/Thy/export_theory.scala	Sun May 13 20:24:33 2018 +0200
     3.3 @@ -11,7 +11,7 @@
     3.4  {
     3.5    /* entities */
     3.6  
     3.7 -  sealed case class Entity(name: String, kind: String, serial: Long, pos: Position.T)
     3.8 +  sealed case class Entity(name: String, serial: Long, pos: Position.T)
     3.9    {
    3.10      override def toString: String = name
    3.11    }
    3.12 @@ -23,10 +23,9 @@
    3.13      tree match {
    3.14        case XML.Elem(Markup(Markup.ENTITY, props), body) =>
    3.15          val name = Markup.Name.unapply(props) getOrElse err()
    3.16 -        val kind = Markup.Kind.unapply(props) getOrElse err()
    3.17          val serial = Markup.Serial.unapply(props) getOrElse err()
    3.18          val pos = props.filter({ case (a, _) => Markup.POSITION_PROPERTIES(a) })
    3.19 -        (Entity(name, kind, serial, pos), body)
    3.20 +        (Entity(name, serial, pos), body)
    3.21        case _ => err()
    3.22      }
    3.23    }