# HG changeset patch # User wenzelm # Date 1606314295 -3600 # Node ID 0cc96d337e8f903845463da857c13d4ee648dbf9 # Parent f1380c9f3806aef8c5175c6d151c1a64f5328f3f tuned signature; diff -r f1380c9f3806 -r 0cc96d337e8f src/Pure/General/position.scala --- a/src/Pure/General/position.scala Wed Nov 25 15:12:02 2020 +0100 +++ b/src/Pure/General/position.scala Wed Nov 25 15:24:55 2020 +0100 @@ -112,14 +112,12 @@ } } - def purge(props: T): T = props.filterNot(p => Markup.POSITION_PROPERTIES(p._1)) - /* here: user output */ def here(props: T, delimited: Boolean = true): String = { - val pos = props.filter(p => Markup.POSITION_PROPERTIES(p._1)) + val pos = props.filter(Markup.position_property) if (pos.isEmpty) "" else { val s0 = diff -r f1380c9f3806 -r 0cc96d337e8f src/Pure/PIDE/command.scala --- a/src/Pure/PIDE/command.scala Wed Nov 25 15:12:02 2020 +0100 +++ b/src/Pure/PIDE/command.scala Wed Nov 25 15:24:55 2020 +0100 @@ -364,7 +364,7 @@ case (Some((target_name, target_chunk)), Position.Range(symbol_range)) => target_chunk.incorporate(symbol_range) match { case Some(range) => - val props = Position.purge(atts) + val props = atts.filterNot(Markup.position_property) val elem = xml_cache.elem(XML.Elem(Markup(name, props), args)) state.add_markup(false, target_name, Text.Info(range, elem)) case None => bad(); state diff -r f1380c9f3806 -r 0cc96d337e8f src/Pure/PIDE/markup.ML --- a/src/Pure/PIDE/markup.ML Wed Nov 25 15:12:02 2020 +0100 +++ b/src/Pure/PIDE/markup.ML Wed Nov 25 15:24:55 2020 +0100 @@ -60,6 +60,7 @@ val fileN: string val idN: string val position_properties: string list + val position_property: Properties.entry -> bool val positionN: string val position: T val expressionN: string val expression: string -> T val citationN: string val citation: string -> T @@ -380,6 +381,7 @@ val idN = "id"; val position_properties = [lineN, offsetN, end_offsetN, fileN, idN]; +fun position_property (entry: Properties.entry) = member (op =) position_properties (#1 entry); val (positionN, position) = markup_elem "position"; diff -r f1380c9f3806 -r 0cc96d337e8f src/Pure/PIDE/markup.scala --- a/src/Pure/PIDE/markup.scala Wed Nov 25 15:12:02 2020 +0100 +++ b/src/Pure/PIDE/markup.scala Wed Nov 25 15:24:55 2020 +0100 @@ -144,6 +144,8 @@ val DEF_ID = "def_id" val POSITION_PROPERTIES = Set(LINE, OFFSET, END_OFFSET, FILE, ID) + def position_property(entry: Properties.Entry): Boolean = POSITION_PROPERTIES(entry._1) + val POSITION = "position" diff -r f1380c9f3806 -r 0cc96d337e8f src/Pure/Thy/export_theory.scala --- a/src/Pure/Thy/export_theory.scala Wed Nov 25 15:12:02 2020 +0100 +++ b/src/Pure/Thy/export_theory.scala Wed Nov 25 15:24:55 2020 +0100 @@ -192,7 +192,7 @@ case XML.Elem(Markup(Markup.ENTITY, props), body) => val name = Markup.Name.unapply(props) getOrElse err() val xname = Markup.XName.unapply(props) getOrElse err() - val pos = props.filter({ case (a, _) => Markup.POSITION_PROPERTIES(a) && a != Markup.ID }) + val pos = props.filter(p => Markup.position_property(p) && p._1 != Markup.ID) val id = Position.Id.unapply(props) val serial = Markup.Serial.unapply(props) getOrElse err() (Entity(kind, name, xname, pos, id, serial), body)