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;
     1 /*  Title:      Pure/General/position.scala
     2     Author:     Makarius
     3 
     4 Position properties.
     5 */
     6 
     7 package isabelle
     8 
     9 
    10 import java.io.{File => JFile}
    11 
    12 
    13 object Position
    14 {
    15   type T = Properties.T
    16 
    17   val none: T = Nil
    18 
    19   val Line = new Properties.Int(Markup.LINE)
    20   val Offset = new Properties.Int(Markup.OFFSET)
    21   val End_Offset = new Properties.Int(Markup.END_OFFSET)
    22   val File = new Properties.String(Markup.FILE)
    23   val Id = new Properties.Long(Markup.ID)
    24   val Id_String = new Properties.String(Markup.ID)
    25 
    26   val Def_Line = new Properties.Int(Markup.DEF_LINE)
    27   val Def_Offset = new Properties.Int(Markup.DEF_OFFSET)
    28   val Def_End_Offset = new Properties.Int(Markup.DEF_END_OFFSET)
    29   val Def_File = new Properties.String(Markup.DEF_FILE)
    30   val Def_Id = new Properties.Long(Markup.DEF_ID)
    31 
    32   object Line_File
    33   {
    34     def apply(line: Int, file: String): T =
    35       (if (line > 0) Line(line) else Nil) :::
    36       (if (file != "") File(file) else Nil)
    37 
    38     def unapply(pos: T): Option[(Int, String)] =
    39       (pos, pos) match {
    40         case (Line(i), File(name)) => Some((i, name))
    41         case (_, File(name)) => Some((1, name))
    42         case _ => None
    43       }
    44   }
    45 
    46   object Def_Line_File
    47   {
    48     def unapply(pos: T): Option[(Int, String)] =
    49       (pos, pos) match {
    50         case (Def_Line(i), Def_File(name)) => Some((i, name))
    51         case (_, Def_File(name)) => Some((1, name))
    52         case _ => None
    53       }
    54   }
    55 
    56   object Range
    57   {
    58     def apply(range: Symbol.Range): T = Offset(range.start) ::: End_Offset(range.stop)
    59     def unapply(pos: T): Option[Symbol.Range] =
    60       (pos, pos) match {
    61         case (Offset(start), End_Offset(stop)) if start <= stop => Some(Text.Range(start, stop))
    62         case (Offset(start), _) => Some(Text.Range(start, start + 1))
    63         case _ => None
    64       }
    65   }
    66 
    67   object Id_Offset0
    68   {
    69     def unapply(pos: T): Option[(Long, Symbol.Offset)] =
    70       pos match {
    71         case Id(id) => Some((id, Offset.unapply(pos) getOrElse 0))
    72         case _ => None
    73       }
    74   }
    75 
    76   object Def_Id_Offset0
    77   {
    78     def unapply(pos: T): Option[(Long, Symbol.Offset)] =
    79       pos match {
    80         case Def_Id(id) => Some((id, Def_Offset.unapply(pos) getOrElse 0))
    81         case _ => None
    82       }
    83   }
    84 
    85   object Identified
    86   {
    87     def unapply(pos: T): Option[(Long, Symbol.Text_Chunk.Name)] =
    88       pos match {
    89         case Id(id) =>
    90           val chunk_name =
    91             pos match {
    92               case File(name) => Symbol.Text_Chunk.File(name)
    93               case _ => Symbol.Text_Chunk.Default
    94             }
    95           Some((id, chunk_name))
    96         case _ => None
    97       }
    98   }
    99 
   100   def purge(props: T): T = props.filterNot(p => Markup.POSITION_PROPERTIES(p._1))
   101 
   102 
   103   /* here: user output */
   104 
   105   def yxml_markup(pos: T, str: String): String =
   106     YXML.string_of_tree(XML.Elem(Markup(Markup.POSITION, pos), List(XML.Text(str))))
   107 
   108   def here(pos: T): String =
   109     yxml_markup(pos,
   110       (Line.unapply(pos), File.unapply(pos)) match {
   111         case (Some(i), None) => " (line " + i.toString + ")"
   112         case (Some(i), Some(name)) => " (line " + i.toString + " of " + quote(name) + ")"
   113         case (None, Some(name)) => " (file " + quote(name) + ")"
   114         case _ => ""
   115       })
   116 
   117   def here_undelimited(pos: T): String =
   118     yxml_markup(pos,
   119       (Line.unapply(pos), File.unapply(pos)) match {
   120         case (Some(i), None) => "line " + i.toString
   121         case (Some(i), Some(name)) => "line " + i.toString + " of " + quote(name)
   122         case (None, Some(name)) => "file " + quote(name)
   123         case _ => ""
   124       })
   125 }