src/Pure/General/position.scala
author wenzelm
Sat, 29 Aug 2009 14:31:39 +0200
changeset 32450 375db037f4d2
parent 31705 0c83e3e75fcf
child 34211 686f828548ef
permissions -rw-r--r--
misc tuning;
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
31705
0c83e3e75fcf replaced java Properties by pure property lists;
wenzelm
parents: 29140
diff changeset
    14
  private def get_string(name: String, pos: T): Option[String] =
0c83e3e75fcf replaced java Properties by pure property lists;
wenzelm
parents: 29140
diff changeset
    15
    pos.find(p => p._1 == name).map(_._2)
0c83e3e75fcf replaced java Properties by pure property lists;
wenzelm
parents: 29140
diff changeset
    16
0c83e3e75fcf replaced java Properties by pure property lists;
wenzelm
parents: 29140
diff changeset
    17
  private def get_int(name: String, pos: T): Option[Int] =
0c83e3e75fcf replaced java Properties by pure property lists;
wenzelm
parents: 29140
diff changeset
    18
  {
0c83e3e75fcf replaced java Properties by pure property lists;
wenzelm
parents: 29140
diff changeset
    19
    get_string(name, pos) match {
27968
85b5f024d94b Position properties.
wenzelm
parents:
diff changeset
    20
      case None => None
85b5f024d94b Position properties.
wenzelm
parents:
diff changeset
    21
      case Some(value) =>
85b5f024d94b Position properties.
wenzelm
parents:
diff changeset
    22
        try { Some(Integer.parseInt(value)) }
27993
6dd90ef9f927 simplified exceptions: use plain error function / RuntimeException;
wenzelm
parents: 27989
diff changeset
    23
        catch { case _: NumberFormatException => None }
27968
85b5f024d94b Position properties.
wenzelm
parents:
diff changeset
    24
    }
85b5f024d94b Position properties.
wenzelm
parents:
diff changeset
    25
  }
85b5f024d94b Position properties.
wenzelm
parents:
diff changeset
    26
31705
0c83e3e75fcf replaced java Properties by pure property lists;
wenzelm
parents: 29140
diff changeset
    27
  def line_of(pos: T) = get_int(Markup.LINE, pos)
0c83e3e75fcf replaced java Properties by pure property lists;
wenzelm
parents: 29140
diff changeset
    28
  def column_of(pos: T) = get_int(Markup.COLUMN, pos)
0c83e3e75fcf replaced java Properties by pure property lists;
wenzelm
parents: 29140
diff changeset
    29
  def offset_of(pos: T) = get_int(Markup.OFFSET, pos)
0c83e3e75fcf replaced java Properties by pure property lists;
wenzelm
parents: 29140
diff changeset
    30
  def end_line_of(pos: T) = get_int(Markup.END_LINE, pos)
0c83e3e75fcf replaced java Properties by pure property lists;
wenzelm
parents: 29140
diff changeset
    31
  def end_column_of(pos: T) = get_int(Markup.END_COLUMN, pos)
0c83e3e75fcf replaced java Properties by pure property lists;
wenzelm
parents: 29140
diff changeset
    32
  def end_offset_of(pos: T) = get_int(Markup.END_OFFSET, pos)
0c83e3e75fcf replaced java Properties by pure property lists;
wenzelm
parents: 29140
diff changeset
    33
  def file_of(pos: T) = get_string(Markup.FILE, pos)
0c83e3e75fcf replaced java Properties by pure property lists;
wenzelm
parents: 29140
diff changeset
    34
  def id_of(pos: T) = get_string(Markup.ID, pos)
0c83e3e75fcf replaced java Properties by pure property lists;
wenzelm
parents: 29140
diff changeset
    35
0c83e3e75fcf replaced java Properties by pure property lists;
wenzelm
parents: 29140
diff changeset
    36
  def offsets_of(pos: T): (Option[Int], Option[Int]) =
0c83e3e75fcf replaced java Properties by pure property lists;
wenzelm
parents: 29140
diff changeset
    37
  {
0c83e3e75fcf replaced java Properties by pure property lists;
wenzelm
parents: 29140
diff changeset
    38
    val begin = offset_of(pos)
0c83e3e75fcf replaced java Properties by pure property lists;
wenzelm
parents: 29140
diff changeset
    39
    val end = end_offset_of(pos)
0c83e3e75fcf replaced java Properties by pure property lists;
wenzelm
parents: 29140
diff changeset
    40
    (begin, if (end.isDefined) end else begin.map(_ + 1))
0c83e3e75fcf replaced java Properties by pure property lists;
wenzelm
parents: 29140
diff changeset
    41
  }
27968
85b5f024d94b Position properties.
wenzelm
parents:
diff changeset
    42
}