src/Pure/General/position.scala
author wenzelm
Sun, 09 Oct 2011 16:47:58 +0200
changeset 45107 76fef3e57004
parent 43780 2cb2310d68b6
child 45666 d83797ef0d2d
permissions -rw-r--r--
tuned;
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
{
43780
2cb2310d68b6 more uniform Properties in ML and Scala;
wenzelm
parents: 43710
diff changeset
    12
  type T = Properties.T
27968
85b5f024d94b Position properties.
wenzelm
parents:
diff changeset
    13
43780
2cb2310d68b6 more uniform Properties in ML and Scala;
wenzelm
parents: 43710
diff changeset
    14
  val Line = new Properties.Int(Markup.LINE)
2cb2310d68b6 more uniform Properties in ML and Scala;
wenzelm
parents: 43710
diff changeset
    15
  val Offset = new Properties.Int(Markup.OFFSET)
2cb2310d68b6 more uniform Properties in ML and Scala;
wenzelm
parents: 43710
diff changeset
    16
  val End_Offset = new Properties.Int(Markup.END_OFFSET)
2cb2310d68b6 more uniform Properties in ML and Scala;
wenzelm
parents: 43710
diff changeset
    17
  val File = new Properties.String(Markup.FILE)
2cb2310d68b6 more uniform Properties in ML and Scala;
wenzelm
parents: 43710
diff changeset
    18
  val Id = new Properties.Long(Markup.ID)
31705
0c83e3e75fcf replaced java Properties by pure property lists;
wenzelm
parents: 29140
diff changeset
    19
38722
ba31936497c2 organized markup properties via apply/unapply patterns;
wenzelm
parents: 38568
diff changeset
    20
  object Range
ba31936497c2 organized markup properties via apply/unapply patterns;
wenzelm
parents: 38568
diff changeset
    21
  {
ba31936497c2 organized markup properties via apply/unapply patterns;
wenzelm
parents: 38568
diff changeset
    22
    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
    23
    def unapply(pos: T): Option[Text.Range] =
ba31936497c2 organized markup properties via apply/unapply patterns;
wenzelm
parents: 38568
diff changeset
    24
      (Offset.unapply(pos), End_Offset.unapply(pos)) match {
ba31936497c2 organized markup properties via apply/unapply patterns;
wenzelm
parents: 38568
diff changeset
    25
        case (Some(start), Some(stop)) if start <= stop => Some(Text.Range(start, stop))
39041
6c8d0ea646a6 Position.Range: exclude singularity (again);
wenzelm
parents: 38887
diff changeset
    26
        case (Some(start), None) => Some(Text.Range(start, start + 1))
38722
ba31936497c2 organized markup properties via apply/unapply patterns;
wenzelm
parents: 38568
diff changeset
    27
        case _ => None
ba31936497c2 organized markup properties via apply/unapply patterns;
wenzelm
parents: 38568
diff changeset
    28
      }
ba31936497c2 organized markup properties via apply/unapply patterns;
wenzelm
parents: 38568
diff changeset
    29
  }
38872
26c505765024 Command.results: ordered by serial number;
wenzelm
parents: 38722
diff changeset
    30
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
    31
  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
    32
  {
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
    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
    34
      (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
    35
        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
    36
        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
    37
      }
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
42327
7c7cc7590eb3 Name_Space.entry_markup: keep def position as separate properties;
wenzelm
parents: 41483
diff changeset
    40
  private val purge_pos = Map(
7c7cc7590eb3 Name_Space.entry_markup: keep def position as separate properties;
wenzelm
parents: 41483
diff changeset
    41
    Markup.DEF_LINE -> Markup.LINE,
7c7cc7590eb3 Name_Space.entry_markup: keep def position as separate properties;
wenzelm
parents: 41483
diff changeset
    42
    Markup.DEF_OFFSET -> Markup.OFFSET,
7c7cc7590eb3 Name_Space.entry_markup: keep def position as separate properties;
wenzelm
parents: 41483
diff changeset
    43
    Markup.DEF_END_OFFSET -> Markup.END_OFFSET,
7c7cc7590eb3 Name_Space.entry_markup: keep def position as separate properties;
wenzelm
parents: 41483
diff changeset
    44
    Markup.DEF_FILE -> Markup.FILE,
7c7cc7590eb3 Name_Space.entry_markup: keep def position as separate properties;
wenzelm
parents: 41483
diff changeset
    45
    Markup.DEF_ID -> Markup.ID)
7c7cc7590eb3 Name_Space.entry_markup: keep def position as separate properties;
wenzelm
parents: 41483
diff changeset
    46
7c7cc7590eb3 Name_Space.entry_markup: keep def position as separate properties;
wenzelm
parents: 41483
diff changeset
    47
  def purge(props: T): T =
7c7cc7590eb3 Name_Space.entry_markup: keep def position as separate properties;
wenzelm
parents: 41483
diff changeset
    48
    for ((x, y) <- props if !Markup.POSITION_PROPERTIES(x))
7c7cc7590eb3 Name_Space.entry_markup: keep def position as separate properties;
wenzelm
parents: 41483
diff changeset
    49
      yield (if (purge_pos.isDefinedAt(x)) (purge_pos(x), y) else (x, y))
27968
85b5f024d94b Position properties.
wenzelm
parents:
diff changeset
    50
}