--- a/src/Pure/General/position.ML Sun May 13 20:04:59 2018 +0200
+++ b/src/Pure/General/position.ML Sun May 13 20:24:33 2018 +0200
@@ -32,6 +32,7 @@
val parse_id: T -> int option
val of_properties: Properties.T -> T
val properties_of: T -> Properties.T
+ val offset_properties_of: T -> Properties.T
val def_properties_of: T -> Properties.T
val entity_properties_of: bool -> serial -> T -> Properties.T
val default_properties: T -> Properties.T -> Properties.T
@@ -161,6 +162,9 @@
fun properties_of (Pos ((i, j, k), props)) =
value Markup.lineN i @ value Markup.offsetN j @ value Markup.end_offsetN k @ props;
+fun offset_properties_of (Pos ((_, j, k), _)) =
+ value Markup.offsetN j @ value Markup.end_offsetN k;
+
val def_properties_of = properties_of #> map (fn (x, y) => ("def_" ^ x, y));
fun entity_properties_of def serial pos =
--- a/src/Pure/Thy/export_theory.ML Sun May 13 20:04:59 2018 +0200
+++ b/src/Pure/Thy/export_theory.ML Sun May 13 20:24:33 2018 +0200
@@ -16,10 +16,9 @@
fun entity_markup space name =
let
- val kind = Name_Space.kind_of space;
val {serial, pos, ...} = Name_Space.the_entry space name;
- val props = Markup.serial_properties serial @ Position.properties_of pos;
- in Markup.properties props (Markup.entity kind name) end;
+ val props = Markup.serial_properties serial @ Position.offset_properties_of pos;
+ in (Markup.entityN, (Markup.nameN, name) :: props) end;
fun export_decls export_decl parents space decls =
(decls, []) |-> fold (fn (name, decl) =>
--- a/src/Pure/Thy/export_theory.scala Sun May 13 20:04:59 2018 +0200
+++ b/src/Pure/Thy/export_theory.scala Sun May 13 20:24:33 2018 +0200
@@ -11,7 +11,7 @@
{
/* entities */
- sealed case class Entity(name: String, kind: String, serial: Long, pos: Position.T)
+ sealed case class Entity(name: String, serial: Long, pos: Position.T)
{
override def toString: String = name
}
@@ -23,10 +23,9 @@
tree match {
case XML.Elem(Markup(Markup.ENTITY, props), body) =>
val name = Markup.Name.unapply(props) getOrElse err()
- val kind = Markup.Kind.unapply(props) getOrElse err()
val serial = Markup.Serial.unapply(props) getOrElse err()
val pos = props.filter({ case (a, _) => Markup.POSITION_PROPERTIES(a) })
- (Entity(name, kind, serial, pos), body)
+ (Entity(name, serial, pos), body)
case _ => err()
}
}