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