src/Pure/General/position.scala
author wenzelm
Tue, 31 Aug 2010 23:28:21 +0200
changeset 38887 1261481ef5e5
parent 38872 26c505765024
child 39041 6c8d0ea646a6
permissions -rw-r--r--
Command.State: add reported positions to markup tree, according main message position or Markup.binding/entity/report occurrences in body; Position.Id_Range convenience;
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
38887
1261481ef5e5 Command.State: add reported positions to markup tree, according main message position or Markup.binding/entity/report occurrences in body;
wenzelm
parents: 38872
diff changeset
    32
  object Id_Range
1261481ef5e5 Command.State: add reported positions to markup tree, according main message position or Markup.binding/entity/report occurrences in body;
wenzelm
parents: 38872
diff changeset
    33
  {
1261481ef5e5 Command.State: add reported positions to markup tree, according main message position or Markup.binding/entity/report occurrences in body;
wenzelm
parents: 38872
diff changeset
    34
    def unapply(pos: T): Option[(Long, Text.Range)] =
1261481ef5e5 Command.State: add reported positions to markup tree, according main message position or Markup.binding/entity/report occurrences in body;
wenzelm
parents: 38872
diff changeset
    35
      (pos, pos) match {
1261481ef5e5 Command.State: add reported positions to markup tree, according main message position or Markup.binding/entity/report occurrences in body;
wenzelm
parents: 38872
diff changeset
    36
        case (Id(id), Range(range)) => Some((id, range))
1261481ef5e5 Command.State: add reported positions to markup tree, according main message position or Markup.binding/entity/report occurrences in body;
wenzelm
parents: 38872
diff changeset
    37
        case _ => None
1261481ef5e5 Command.State: add reported positions to markup tree, according main message position or Markup.binding/entity/report occurrences in body;
wenzelm
parents: 38872
diff changeset
    38
      }
1261481ef5e5 Command.State: add reported positions to markup tree, according main message position or Markup.binding/entity/report occurrences in body;
wenzelm
parents: 38872
diff changeset
    39
  }
1261481ef5e5 Command.State: add reported positions to markup tree, according main message position or Markup.binding/entity/report occurrences in body;
wenzelm
parents: 38872
diff changeset
    40
38872
26c505765024 Command.results: ordered by serial number;
wenzelm
parents: 38722
diff changeset
    41
  def purge(props: T): T = props.filterNot(p => Markup.POSITION_PROPERTIES(p._1))
27968
85b5f024d94b Position properties.
wenzelm
parents:
diff changeset
    42
}