src/Pure/General/position.scala
author wenzelm
Mon, 30 Aug 2010 13:01:32 +0200
changeset 38872 26c505765024
parent 38722 ba31936497c2
child 38887 1261481ef5e5
permissions -rw-r--r--
Command.results: ordered by serial number;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
27968
85b5f024d94b Position properties.
wenzelm
parents:
diff changeset
     1
/*  Title:      Pure/General/position.scala
85b5f024d94b Position properties.
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
85b5f024d94b Position properties.
wenzelm
parents:
diff changeset
     3
85b5f024d94b Position properties.
wenzelm
parents:
diff changeset
     4
Position properties.
85b5f024d94b Position properties.
wenzelm
parents:
diff changeset
     5
*/
85b5f024d94b Position properties.
wenzelm
parents:
diff changeset
     6
85b5f024d94b Position properties.
wenzelm
parents:
diff changeset
     7
package isabelle
85b5f024d94b Position properties.
wenzelm
parents:
diff changeset
     8
85b5f024d94b Position properties.
wenzelm
parents:
diff changeset
     9
32450
375db037f4d2 misc tuning;
wenzelm
parents: 31705
diff changeset
    10
object Position
375db037f4d2 misc tuning;
wenzelm
parents: 31705
diff changeset
    11
{
31705
0c83e3e75fcf replaced java Properties by pure property lists;
wenzelm
parents: 29140
diff changeset
    12
  type T = List[(String, String)]
27968
85b5f024d94b Position properties.
wenzelm
parents:
diff changeset
    13
38722
ba31936497c2 organized markup properties via apply/unapply patterns;
wenzelm
parents: 38568
diff changeset
    14
  val Line = new Markup.Int_Property(Markup.LINE)
ba31936497c2 organized markup properties via apply/unapply patterns;
wenzelm
parents: 38568
diff changeset
    15
  val End_Line = new Markup.Int_Property(Markup.END_LINE)
ba31936497c2 organized markup properties via apply/unapply patterns;
wenzelm
parents: 38568
diff changeset
    16
  val Offset = new Markup.Int_Property(Markup.OFFSET)
ba31936497c2 organized markup properties via apply/unapply patterns;
wenzelm
parents: 38568
diff changeset
    17
  val End_Offset = new Markup.Int_Property(Markup.END_OFFSET)
ba31936497c2 organized markup properties via apply/unapply patterns;
wenzelm
parents: 38568
diff changeset
    18
  val File = new Markup.Property(Markup.FILE)
ba31936497c2 organized markup properties via apply/unapply patterns;
wenzelm
parents: 38568
diff changeset
    19
  val Id = new Markup.Long_Property(Markup.ID)
31705
0c83e3e75fcf replaced java Properties by pure property lists;
wenzelm
parents: 29140
diff changeset
    20
38722
ba31936497c2 organized markup properties via apply/unapply patterns;
wenzelm
parents: 38568
diff changeset
    21
  object Range
ba31936497c2 organized markup properties via apply/unapply patterns;
wenzelm
parents: 38568
diff changeset
    22
  {
ba31936497c2 organized markup properties via apply/unapply patterns;
wenzelm
parents: 38568
diff changeset
    23
    def apply(range: Text.Range): T = Offset(range.start) ++ Offset(range.stop)
ba31936497c2 organized markup properties via apply/unapply patterns;
wenzelm
parents: 38568
diff changeset
    24
    def unapply(pos: T): Option[Text.Range] =
ba31936497c2 organized markup properties via apply/unapply patterns;
wenzelm
parents: 38568
diff changeset
    25
      (Offset.unapply(pos), End_Offset.unapply(pos)) match {
ba31936497c2 organized markup properties via apply/unapply patterns;
wenzelm
parents: 38568
diff changeset
    26
        case (Some(start), Some(stop)) if start <= stop => Some(Text.Range(start, stop))
ba31936497c2 organized markup properties via apply/unapply patterns;
wenzelm
parents: 38568
diff changeset
    27
        case (Some(start), None) => Some(Text.Range(start))
ba31936497c2 organized markup properties via apply/unapply patterns;
wenzelm
parents: 38568
diff changeset
    28
        case _ => None
ba31936497c2 organized markup properties via apply/unapply patterns;
wenzelm
parents: 38568
diff changeset
    29
      }
ba31936497c2 organized markup properties via apply/unapply patterns;
wenzelm
parents: 38568
diff changeset
    30
  }
38872
26c505765024 Command.results: ordered by serial number;
wenzelm
parents: 38722
diff changeset
    31
26c505765024 Command.results: ordered by serial number;
wenzelm
parents: 38722
diff changeset
    32
  def purge(props: T): T = props.filterNot(p => Markup.POSITION_PROPERTIES(p._1))
27968
85b5f024d94b Position properties.
wenzelm
parents:
diff changeset
    33
}