Renamed upd_snd_conv to apsnd_conv to be consistent with apfst_conv; Added apsnd_apfst_commute
/* Title: Pure/General/position.scala
Author: Makarius
Position properties.
*/
package isabelle
object Position
{
type T = List[(String, String)]
private def get_string(name: String, pos: T): Option[String] =
pos.find(p => p._1 == name).map(_._2)
private def get_int(name: String, pos: T): Option[Int] =
{
get_string(name, pos) match {
case None => None
case Some(value) =>
try { Some(Integer.parseInt(value)) }
catch { case _: NumberFormatException => None }
}
}
def line_of(pos: T) = get_int(Markup.LINE, pos)
def column_of(pos: T) = get_int(Markup.COLUMN, pos)
def offset_of(pos: T) = get_int(Markup.OFFSET, pos)
def end_line_of(pos: T) = get_int(Markup.END_LINE, pos)
def end_column_of(pos: T) = get_int(Markup.END_COLUMN, pos)
def end_offset_of(pos: T) = get_int(Markup.END_OFFSET, pos)
def file_of(pos: T) = get_string(Markup.FILE, pos)
def id_of(pos: T) = get_string(Markup.ID, pos)
def offsets_of(pos: T): (Option[Int], Option[Int]) =
{
val begin = offset_of(pos)
val end = end_offset_of(pos)
(begin, if (end.isDefined) end else begin.map(_ + 1))
}
}