src/Pure/General/position.scala
author wenzelm
Sun Mar 15 21:57:10 2015 +0100 (2015-03-15)
changeset 59706 bf6ca55aae13
parent 59671 9715eb8e9408
child 59707 10effab11669
permissions -rw-r--r--
proper command id for inlined errors, which is important for Command.State.accumulate;
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@55490
    17
  val none: T = Nil
wenzelm@55490
    18
wenzelm@50201
    19
  val Line = new Properties.Int(Markup.LINE)
wenzelm@50201
    20
  val Offset = new Properties.Int(Markup.OFFSET)
wenzelm@50201
    21
  val End_Offset = new Properties.Int(Markup.END_OFFSET)
wenzelm@50201
    22
  val File = new Properties.String(Markup.FILE)
wenzelm@50201
    23
  val Id = new Properties.Long(Markup.ID)
wenzelm@59706
    24
  val Id_String = new Properties.String(Markup.ID)
wenzelm@31705
    25
wenzelm@50201
    26
  val Def_Line = new Properties.Int(Markup.DEF_LINE)
wenzelm@50201
    27
  val Def_Offset = new Properties.Int(Markup.DEF_OFFSET)
wenzelm@50201
    28
  val Def_End_Offset = new Properties.Int(Markup.DEF_END_OFFSET)
wenzelm@50201
    29
  val Def_File = new Properties.String(Markup.DEF_FILE)
wenzelm@50201
    30
  val Def_Id = new Properties.Long(Markup.DEF_ID)
wenzelm@49419
    31
wenzelm@48920
    32
  object Line_File
wenzelm@48920
    33
  {
wenzelm@56464
    34
    def apply(line: Int, file: String): T =
wenzelm@56464
    35
      (if (line > 0) Line(line) else Nil) :::
wenzelm@56464
    36
      (if (file != "") File(file) else Nil)
wenzelm@56464
    37
wenzelm@48920
    38
    def unapply(pos: T): Option[(Int, String)] =
wenzelm@48920
    39
      (pos, pos) match {
wenzelm@48920
    40
        case (Line(i), File(name)) => Some((i, name))
wenzelm@48920
    41
        case (_, File(name)) => Some((1, name))
wenzelm@48920
    42
        case _ => None
wenzelm@48920
    43
      }
wenzelm@48920
    44
  }
wenzelm@48920
    45
wenzelm@49419
    46
  object Def_Line_File
wenzelm@49419
    47
  {
wenzelm@49419
    48
    def unapply(pos: T): Option[(Int, String)] =
wenzelm@49419
    49
      (pos, pos) match {
wenzelm@49419
    50
        case (Def_Line(i), Def_File(name)) => Some((i, name))
wenzelm@49419
    51
        case (_, Def_File(name)) => Some((1, name))
wenzelm@49419
    52
        case _ => None
wenzelm@49419
    53
      }
wenzelm@49419
    54
  }
wenzelm@49419
    55
wenzelm@38722
    56
  object Range
wenzelm@38722
    57
  {
wenzelm@57910
    58
    def apply(range: Symbol.Range): T = Offset(range.start) ::: End_Offset(range.stop)
wenzelm@55884
    59
    def unapply(pos: T): Option[Symbol.Range] =
wenzelm@48920
    60
      (pos, pos) match {
wenzelm@48920
    61
        case (Offset(start), End_Offset(stop)) if start <= stop => Some(Text.Range(start, stop))
wenzelm@48920
    62
        case (Offset(start), _) => Some(Text.Range(start, start + 1))
wenzelm@48920
    63
        case _ => None
wenzelm@48920
    64
      }
wenzelm@48920
    65
  }
wenzelm@48920
    66
wenzelm@57931
    67
  object Id_Offset0
wenzelm@48920
    68
  {
wenzelm@55884
    69
    def unapply(pos: T): Option[(Long, Symbol.Offset)] =
wenzelm@57931
    70
      pos match {
wenzelm@57931
    71
        case Id(id) => Some((id, Offset.unapply(pos) getOrElse 0))
wenzelm@38722
    72
        case _ => None
wenzelm@38722
    73
      }
wenzelm@38722
    74
  }
wenzelm@38872
    75
wenzelm@57931
    76
  object Def_Id_Offset0
wenzelm@49419
    77
  {
wenzelm@55884
    78
    def unapply(pos: T): Option[(Long, Symbol.Offset)] =
wenzelm@57931
    79
      pos match {
wenzelm@57931
    80
        case Def_Id(id) => Some((id, Def_Offset.unapply(pos) getOrElse 0))
wenzelm@49419
    81
        case _ => None
wenzelm@49419
    82
      }
wenzelm@49419
    83
  }
wenzelm@49419
    84
wenzelm@57911
    85
  object Identified
wenzelm@38887
    86
  {
wenzelm@57911
    87
    def unapply(pos: T): Option[(Long, Symbol.Text_Chunk.Name)] =
wenzelm@57911
    88
      pos match {
wenzelm@57911
    89
        case Id(id) =>
wenzelm@56462
    90
          val chunk_name =
wenzelm@56462
    91
            pos match {
wenzelm@56746
    92
              case File(name) => Symbol.Text_Chunk.File(name)
wenzelm@56746
    93
              case _ => Symbol.Text_Chunk.Default
wenzelm@56462
    94
            }
wenzelm@57911
    95
          Some((id, chunk_name))
wenzelm@38887
    96
        case _ => None
wenzelm@38887
    97
      }
wenzelm@38887
    98
  }
wenzelm@38887
    99
wenzelm@50201
   100
  def purge(props: T): T = props.filterNot(p => Markup.POSITION_PROPERTIES(p._1))
wenzelm@48370
   101
wenzelm@48370
   102
wenzelm@56532
   103
  /* here: user output */
wenzelm@48992
   104
wenzelm@59671
   105
  def yxml_markup(pos: T, str: String): String =
wenzelm@59671
   106
    YXML.string_of_tree(XML.Elem(Markup(Markup.POSITION, pos), List(XML.Text(str))))
wenzelm@59671
   107
wenzelm@48992
   108
  def here(pos: T): String =
wenzelm@59671
   109
    yxml_markup(pos,
wenzelm@59671
   110
      (Line.unapply(pos), File.unapply(pos)) match {
wenzelm@59671
   111
        case (Some(i), None) => " (line " + i.toString + ")"
wenzelm@59671
   112
        case (Some(i), Some(name)) => " (line " + i.toString + " of " + quote(name) + ")"
wenzelm@59671
   113
        case (None, Some(name)) => " (file " + quote(name) + ")"
wenzelm@59671
   114
        case _ => ""
wenzelm@59671
   115
      })
wenzelm@56532
   116
wenzelm@56532
   117
  def here_undelimited(pos: T): String =
wenzelm@59671
   118
    yxml_markup(pos,
wenzelm@59671
   119
      (Line.unapply(pos), File.unapply(pos)) match {
wenzelm@59671
   120
        case (Some(i), None) => "line " + i.toString
wenzelm@59671
   121
        case (Some(i), Some(name)) => "line " + i.toString + " of " + quote(name)
wenzelm@59671
   122
        case (None, Some(name)) => "file " + quote(name)
wenzelm@59671
   123
        case _ => ""
wenzelm@59671
   124
      })
wenzelm@27968
   125
}