src/Pure/General/position.scala
author wenzelm
Wed Aug 13 22:29:43 2014 +0200 (2014-08-13)
changeset 57931 4e2cbff02f23
parent 57911 dcb758188aa6
child 59671 9715eb8e9408
permissions -rw-r--r--
tuned;
     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 
    25   val Def_Line = new Properties.Int(Markup.DEF_LINE)
    26   val Def_Offset = new Properties.Int(Markup.DEF_OFFSET)
    27   val Def_End_Offset = new Properties.Int(Markup.DEF_END_OFFSET)
    28   val Def_File = new Properties.String(Markup.DEF_FILE)
    29   val Def_Id = new Properties.Long(Markup.DEF_ID)
    30 
    31   object Line_File
    32   {
    33     def apply(line: Int, file: String): T =
    34       (if (line > 0) Line(line) else Nil) :::
    35       (if (file != "") File(file) else Nil)
    36 
    37     def unapply(pos: T): Option[(Int, String)] =
    38       (pos, pos) match {
    39         case (Line(i), File(name)) => Some((i, name))
    40         case (_, File(name)) => Some((1, name))
    41         case _ => None
    42       }
    43   }
    44 
    45   object Def_Line_File
    46   {
    47     def unapply(pos: T): Option[(Int, String)] =
    48       (pos, pos) match {
    49         case (Def_Line(i), Def_File(name)) => Some((i, name))
    50         case (_, Def_File(name)) => Some((1, name))
    51         case _ => None
    52       }
    53   }
    54 
    55   object Range
    56   {
    57     def apply(range: Symbol.Range): T = Offset(range.start) ::: End_Offset(range.stop)
    58     def unapply(pos: T): Option[Symbol.Range] =
    59       (pos, pos) match {
    60         case (Offset(start), End_Offset(stop)) if start <= stop => Some(Text.Range(start, stop))
    61         case (Offset(start), _) => Some(Text.Range(start, start + 1))
    62         case _ => None
    63       }
    64   }
    65 
    66   object Id_Offset0
    67   {
    68     def unapply(pos: T): Option[(Long, Symbol.Offset)] =
    69       pos match {
    70         case Id(id) => Some((id, Offset.unapply(pos) getOrElse 0))
    71         case _ => None
    72       }
    73   }
    74 
    75   object Def_Id_Offset0
    76   {
    77     def unapply(pos: T): Option[(Long, Symbol.Offset)] =
    78       pos match {
    79         case Def_Id(id) => Some((id, Def_Offset.unapply(pos) getOrElse 0))
    80         case _ => None
    81       }
    82   }
    83 
    84   object Identified
    85   {
    86     def unapply(pos: T): Option[(Long, Symbol.Text_Chunk.Name)] =
    87       pos match {
    88         case Id(id) =>
    89           val chunk_name =
    90             pos match {
    91               case File(name) => Symbol.Text_Chunk.File(name)
    92               case _ => Symbol.Text_Chunk.Default
    93             }
    94           Some((id, chunk_name))
    95         case _ => None
    96       }
    97   }
    98 
    99   def purge(props: T): T = props.filterNot(p => Markup.POSITION_PROPERTIES(p._1))
   100 
   101 
   102   /* here: user output */
   103 
   104   def here(pos: T): String =
   105     (Line.unapply(pos), File.unapply(pos)) match {
   106       case (Some(i), None) => " (line " + i.toString + ")"
   107       case (Some(i), Some(name)) => " (line " + i.toString + " of " + quote(name) + ")"
   108       case (None, Some(name)) => " (file " + quote(name) + ")"
   109       case _ => ""
   110     }
   111 
   112   def here_undelimited(pos: T): String =
   113     (Line.unapply(pos), File.unapply(pos)) match {
   114       case (Some(i), None) => "line " + i.toString
   115       case (Some(i), Some(name)) => "line " + i.toString + " of " + quote(name)
   116       case (None, Some(name)) => "file " + quote(name)
   117       case _ => ""
   118     }
   119 }