src/Pure/General/position.scala
author wenzelm
Fri Jul 20 22:29:25 2012 +0200 (2012-07-20)
changeset 48409 0d2114eb412a
parent 48370 d0fa3efec93b
child 48548 49afe0e92163
permissions -rw-r--r--
more explicit java.io.{File => JFile};
wenzelm@27968
     1
/*  Title:      Pure/General/position.scala
wenzelm@27968
     2
    Author:     Makarius
wenzelm@27968
     3
wenzelm@27968
     4
Position properties.
wenzelm@27968
     5
*/
wenzelm@27968
     6
wenzelm@27968
     7
package isabelle
wenzelm@27968
     8
wenzelm@27968
     9
wenzelm@48409
    10
import java.io.{File => JFile}
wenzelm@48409
    11
wenzelm@48409
    12
wenzelm@32450
    13
object Position
wenzelm@32450
    14
{
wenzelm@43780
    15
  type T = Properties.T
wenzelm@27968
    16
wenzelm@45666
    17
  val Line = new Properties.Int(Isabelle_Markup.LINE)
wenzelm@45666
    18
  val Offset = new Properties.Int(Isabelle_Markup.OFFSET)
wenzelm@45666
    19
  val End_Offset = new Properties.Int(Isabelle_Markup.END_OFFSET)
wenzelm@45666
    20
  val File = new Properties.String(Isabelle_Markup.FILE)
wenzelm@45666
    21
  val Id = new Properties.Long(Isabelle_Markup.ID)
wenzelm@31705
    22
wenzelm@48409
    23
  def file(f: JFile): T = File(Isabelle_System.posix_path(f.toString))
wenzelm@48409
    24
  def line_file(i: Int, f: JFile): T = Line(i) ::: file(f)
wenzelm@48370
    25
wenzelm@38722
    26
  object Range
wenzelm@38722
    27
  {
wenzelm@38722
    28
    def apply(range: Text.Range): T = Offset(range.start) ++ Offset(range.stop)
wenzelm@38722
    29
    def unapply(pos: T): Option[Text.Range] =
wenzelm@38722
    30
      (Offset.unapply(pos), End_Offset.unapply(pos)) match {
wenzelm@38722
    31
        case (Some(start), Some(stop)) if start <= stop => Some(Text.Range(start, stop))
wenzelm@39041
    32
        case (Some(start), None) => Some(Text.Range(start, start + 1))
wenzelm@38722
    33
        case _ => None
wenzelm@38722
    34
      }
wenzelm@38722
    35
  }
wenzelm@38872
    36
wenzelm@38887
    37
  object Id_Range
wenzelm@38887
    38
  {
wenzelm@38887
    39
    def unapply(pos: T): Option[(Long, Text.Range)] =
wenzelm@38887
    40
      (pos, pos) match {
wenzelm@38887
    41
        case (Id(id), Range(range)) => Some((id, range))
wenzelm@38887
    42
        case _ => None
wenzelm@38887
    43
      }
wenzelm@38887
    44
  }
wenzelm@38887
    45
wenzelm@42327
    46
  private val purge_pos = Map(
wenzelm@45666
    47
    Isabelle_Markup.DEF_LINE -> Isabelle_Markup.LINE,
wenzelm@45666
    48
    Isabelle_Markup.DEF_OFFSET -> Isabelle_Markup.OFFSET,
wenzelm@45666
    49
    Isabelle_Markup.DEF_END_OFFSET -> Isabelle_Markup.END_OFFSET,
wenzelm@45666
    50
    Isabelle_Markup.DEF_FILE -> Isabelle_Markup.FILE,
wenzelm@45666
    51
    Isabelle_Markup.DEF_ID -> Isabelle_Markup.ID)
wenzelm@42327
    52
wenzelm@42327
    53
  def purge(props: T): T =
wenzelm@45666
    54
    for ((x, y) <- props if !Isabelle_Markup.POSITION_PROPERTIES(x))
wenzelm@42327
    55
      yield (if (purge_pos.isDefinedAt(x)) (purge_pos(x), y) else (x, y))
wenzelm@48370
    56
wenzelm@48370
    57
wenzelm@48370
    58
  def str_of(props: T): String =
wenzelm@48370
    59
    (Line.unapply(props), File.unapply(props)) match {
wenzelm@48370
    60
      case (Some(i), None) => " (line " + i.toString + ")"
wenzelm@48370
    61
      case (Some(i), Some(name)) => " (line " + i.toString + " of " + quote(name) + ")"
wenzelm@48370
    62
      case (None, Some(name)) => " (file " + quote(name) + ")"
wenzelm@48370
    63
      case _ => ""
wenzelm@48370
    64
    }
wenzelm@27968
    65
}