src/Pure/General/position.scala
author wenzelm
Mon Aug 30 13:01:32 2010 +0200 (2010-08-30)
changeset 38872 26c505765024
parent 38722 ba31936497c2
child 38887 1261481ef5e5
permissions -rw-r--r--
Command.results: ordered by serial number;
     1 /*  Title:      Pure/General/position.scala
     2     Author:     Makarius
     3 
     4 Position properties.
     5 */
     6 
     7 package isabelle
     8 
     9 
    10 object Position
    11 {
    12   type T = List[(String, String)]
    13 
    14   val Line = new Markup.Int_Property(Markup.LINE)
    15   val End_Line = new Markup.Int_Property(Markup.END_LINE)
    16   val Offset = new Markup.Int_Property(Markup.OFFSET)
    17   val End_Offset = new Markup.Int_Property(Markup.END_OFFSET)
    18   val File = new Markup.Property(Markup.FILE)
    19   val Id = new Markup.Long_Property(Markup.ID)
    20 
    21   object Range
    22   {
    23     def apply(range: Text.Range): T = Offset(range.start) ++ Offset(range.stop)
    24     def unapply(pos: T): Option[Text.Range] =
    25       (Offset.unapply(pos), End_Offset.unapply(pos)) match {
    26         case (Some(start), Some(stop)) if start <= stop => Some(Text.Range(start, stop))
    27         case (Some(start), None) => Some(Text.Range(start))
    28         case _ => None
    29       }
    30   }
    31 
    32   def purge(props: T): T = props.filterNot(p => Markup.POSITION_PROPERTIES(p._1))
    33 }