src/Pure/General/position.scala
author wenzelm
Tue, 18 Sep 2012 19:33:45 +0200
changeset 49419 e2726211f834
parent 48992 0518bf89c777
child 50201 c26369c9eda6
permissions -rw-r--r--
pass base_snapshot to enable hyperlinks into other nodes; clarified "def" positions: refrain from renaming properties; clarified snapshot.is_output vs. output and hyperlinks;
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
48409
0d2114eb412a more explicit java.io.{File => JFile};
wenzelm
parents: 48370
diff changeset
    10
import java.io.{File => JFile}
0d2114eb412a more explicit java.io.{File => JFile};
wenzelm
parents: 48370
diff changeset
    11
0d2114eb412a more explicit java.io.{File => JFile};
wenzelm
parents: 48370
diff changeset
    12
32450
375db037f4d2 misc tuning;
wenzelm
parents: 31705
diff changeset
    13
object Position
375db037f4d2 misc tuning;
wenzelm
parents: 31705
diff changeset
    14
{
43780
2cb2310d68b6 more uniform Properties in ML and Scala;
wenzelm
parents: 43710
diff changeset
    15
  type T = Properties.T
27968
85b5f024d94b Position properties.
wenzelm
parents:
diff changeset
    16
45666
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 43780
diff changeset
    17
  val Line = new Properties.Int(Isabelle_Markup.LINE)
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 43780
diff changeset
    18
  val Offset = new Properties.Int(Isabelle_Markup.OFFSET)
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 43780
diff changeset
    19
  val End_Offset = new Properties.Int(Isabelle_Markup.END_OFFSET)
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 43780
diff changeset
    20
  val File = new Properties.String(Isabelle_Markup.FILE)
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 43780
diff changeset
    21
  val Id = new Properties.Long(Isabelle_Markup.ID)
31705
0c83e3e75fcf replaced java Properties by pure property lists;
wenzelm
parents: 29140
diff changeset
    22
49419
e2726211f834 pass base_snapshot to enable hyperlinks into other nodes;
wenzelm
parents: 48992
diff changeset
    23
  val Def_Line = new Properties.Int(Isabelle_Markup.DEF_LINE)
e2726211f834 pass base_snapshot to enable hyperlinks into other nodes;
wenzelm
parents: 48992
diff changeset
    24
  val Def_Offset = new Properties.Int(Isabelle_Markup.DEF_OFFSET)
e2726211f834 pass base_snapshot to enable hyperlinks into other nodes;
wenzelm
parents: 48992
diff changeset
    25
  val Def_End_Offset = new Properties.Int(Isabelle_Markup.DEF_END_OFFSET)
e2726211f834 pass base_snapshot to enable hyperlinks into other nodes;
wenzelm
parents: 48992
diff changeset
    26
  val Def_File = new Properties.String(Isabelle_Markup.DEF_FILE)
e2726211f834 pass base_snapshot to enable hyperlinks into other nodes;
wenzelm
parents: 48992
diff changeset
    27
  val Def_Id = new Properties.Long(Isabelle_Markup.DEF_ID)
e2726211f834 pass base_snapshot to enable hyperlinks into other nodes;
wenzelm
parents: 48992
diff changeset
    28
48920
9f84d872feba tuned signature;
wenzelm
parents: 48548
diff changeset
    29
  object Line_File
9f84d872feba tuned signature;
wenzelm
parents: 48548
diff changeset
    30
  {
9f84d872feba tuned signature;
wenzelm
parents: 48548
diff changeset
    31
    def unapply(pos: T): Option[(Int, String)] =
9f84d872feba tuned signature;
wenzelm
parents: 48548
diff changeset
    32
      (pos, pos) match {
9f84d872feba tuned signature;
wenzelm
parents: 48548
diff changeset
    33
        case (Line(i), File(name)) => Some((i, name))
9f84d872feba tuned signature;
wenzelm
parents: 48548
diff changeset
    34
        case (_, File(name)) => Some((1, name))
9f84d872feba tuned signature;
wenzelm
parents: 48548
diff changeset
    35
        case _ => None
9f84d872feba tuned signature;
wenzelm
parents: 48548
diff changeset
    36
      }
9f84d872feba tuned signature;
wenzelm
parents: 48548
diff changeset
    37
  }
9f84d872feba tuned signature;
wenzelm
parents: 48548
diff changeset
    38
49419
e2726211f834 pass base_snapshot to enable hyperlinks into other nodes;
wenzelm
parents: 48992
diff changeset
    39
  object Def_Line_File
e2726211f834 pass base_snapshot to enable hyperlinks into other nodes;
wenzelm
parents: 48992
diff changeset
    40
  {
e2726211f834 pass base_snapshot to enable hyperlinks into other nodes;
wenzelm
parents: 48992
diff changeset
    41
    def unapply(pos: T): Option[(Int, String)] =
e2726211f834 pass base_snapshot to enable hyperlinks into other nodes;
wenzelm
parents: 48992
diff changeset
    42
      (pos, pos) match {
e2726211f834 pass base_snapshot to enable hyperlinks into other nodes;
wenzelm
parents: 48992
diff changeset
    43
        case (Def_Line(i), Def_File(name)) => Some((i, name))
e2726211f834 pass base_snapshot to enable hyperlinks into other nodes;
wenzelm
parents: 48992
diff changeset
    44
        case (_, Def_File(name)) => Some((1, name))
e2726211f834 pass base_snapshot to enable hyperlinks into other nodes;
wenzelm
parents: 48992
diff changeset
    45
        case _ => None
e2726211f834 pass base_snapshot to enable hyperlinks into other nodes;
wenzelm
parents: 48992
diff changeset
    46
      }
e2726211f834 pass base_snapshot to enable hyperlinks into other nodes;
wenzelm
parents: 48992
diff changeset
    47
  }
e2726211f834 pass base_snapshot to enable hyperlinks into other nodes;
wenzelm
parents: 48992
diff changeset
    48
38722
ba31936497c2 organized markup properties via apply/unapply patterns;
wenzelm
parents: 38568
diff changeset
    49
  object Range
ba31936497c2 organized markup properties via apply/unapply patterns;
wenzelm
parents: 38568
diff changeset
    50
  {
ba31936497c2 organized markup properties via apply/unapply patterns;
wenzelm
parents: 38568
diff changeset
    51
    def apply(range: Text.Range): T = Offset(range.start) ++ Offset(range.stop)
ba31936497c2 organized markup properties via apply/unapply patterns;
wenzelm
parents: 38568
diff changeset
    52
    def unapply(pos: T): Option[Text.Range] =
48920
9f84d872feba tuned signature;
wenzelm
parents: 48548
diff changeset
    53
      (pos, pos) match {
9f84d872feba tuned signature;
wenzelm
parents: 48548
diff changeset
    54
        case (Offset(start), End_Offset(stop)) if start <= stop => Some(Text.Range(start, stop))
9f84d872feba tuned signature;
wenzelm
parents: 48548
diff changeset
    55
        case (Offset(start), _) => Some(Text.Range(start, start + 1))
9f84d872feba tuned signature;
wenzelm
parents: 48548
diff changeset
    56
        case _ => None
9f84d872feba tuned signature;
wenzelm
parents: 48548
diff changeset
    57
      }
9f84d872feba tuned signature;
wenzelm
parents: 48548
diff changeset
    58
  }
9f84d872feba tuned signature;
wenzelm
parents: 48548
diff changeset
    59
9f84d872feba tuned signature;
wenzelm
parents: 48548
diff changeset
    60
  object Id_Offset
9f84d872feba tuned signature;
wenzelm
parents: 48548
diff changeset
    61
  {
9f84d872feba tuned signature;
wenzelm
parents: 48548
diff changeset
    62
    def unapply(pos: T): Option[(Long, Text.Offset)] =
9f84d872feba tuned signature;
wenzelm
parents: 48548
diff changeset
    63
      (pos, pos) match {
9f84d872feba tuned signature;
wenzelm
parents: 48548
diff changeset
    64
        case (Id(id), Offset(offset)) => Some((id, offset))
38722
ba31936497c2 organized markup properties via apply/unapply patterns;
wenzelm
parents: 38568
diff changeset
    65
        case _ => None
ba31936497c2 organized markup properties via apply/unapply patterns;
wenzelm
parents: 38568
diff changeset
    66
      }
ba31936497c2 organized markup properties via apply/unapply patterns;
wenzelm
parents: 38568
diff changeset
    67
  }
38872
26c505765024 Command.results: ordered by serial number;
wenzelm
parents: 38722
diff changeset
    68
49419
e2726211f834 pass base_snapshot to enable hyperlinks into other nodes;
wenzelm
parents: 48992
diff changeset
    69
  object Def_Id_Offset
e2726211f834 pass base_snapshot to enable hyperlinks into other nodes;
wenzelm
parents: 48992
diff changeset
    70
  {
e2726211f834 pass base_snapshot to enable hyperlinks into other nodes;
wenzelm
parents: 48992
diff changeset
    71
    def unapply(pos: T): Option[(Long, Text.Offset)] =
e2726211f834 pass base_snapshot to enable hyperlinks into other nodes;
wenzelm
parents: 48992
diff changeset
    72
      (pos, pos) match {
e2726211f834 pass base_snapshot to enable hyperlinks into other nodes;
wenzelm
parents: 48992
diff changeset
    73
        case (Def_Id(id), Def_Offset(offset)) => Some((id, offset))
e2726211f834 pass base_snapshot to enable hyperlinks into other nodes;
wenzelm
parents: 48992
diff changeset
    74
        case _ => None
e2726211f834 pass base_snapshot to enable hyperlinks into other nodes;
wenzelm
parents: 48992
diff changeset
    75
      }
e2726211f834 pass base_snapshot to enable hyperlinks into other nodes;
wenzelm
parents: 48992
diff changeset
    76
  }
e2726211f834 pass base_snapshot to enable hyperlinks into other nodes;
wenzelm
parents: 48992
diff changeset
    77
38887
1261481ef5e5 Command.State: add reported positions to markup tree, according main message position or Markup.binding/entity/report occurrences in body;
wenzelm
parents: 38872
diff changeset
    78
  object Id_Range
1261481ef5e5 Command.State: add reported positions to markup tree, according main message position or Markup.binding/entity/report occurrences in body;
wenzelm
parents: 38872
diff changeset
    79
  {
1261481ef5e5 Command.State: add reported positions to markup tree, according main message position or Markup.binding/entity/report occurrences in body;
wenzelm
parents: 38872
diff changeset
    80
    def unapply(pos: T): Option[(Long, Text.Range)] =
1261481ef5e5 Command.State: add reported positions to markup tree, according main message position or Markup.binding/entity/report occurrences in body;
wenzelm
parents: 38872
diff changeset
    81
      (pos, pos) match {
1261481ef5e5 Command.State: add reported positions to markup tree, according main message position or Markup.binding/entity/report occurrences in body;
wenzelm
parents: 38872
diff changeset
    82
        case (Id(id), Range(range)) => Some((id, range))
1261481ef5e5 Command.State: add reported positions to markup tree, according main message position or Markup.binding/entity/report occurrences in body;
wenzelm
parents: 38872
diff changeset
    83
        case _ => None
1261481ef5e5 Command.State: add reported positions to markup tree, according main message position or Markup.binding/entity/report occurrences in body;
wenzelm
parents: 38872
diff changeset
    84
      }
1261481ef5e5 Command.State: add reported positions to markup tree, according main message position or Markup.binding/entity/report occurrences in body;
wenzelm
parents: 38872
diff changeset
    85
  }
1261481ef5e5 Command.State: add reported positions to markup tree, according main message position or Markup.binding/entity/report occurrences in body;
wenzelm
parents: 38872
diff changeset
    86
49419
e2726211f834 pass base_snapshot to enable hyperlinks into other nodes;
wenzelm
parents: 48992
diff changeset
    87
  def purge(props: T): T = props.filterNot(p => Isabelle_Markup.POSITION_PROPERTIES(p._1))
48370
d0fa3efec93b require explicit initialization of options;
wenzelm
parents: 45666
diff changeset
    88
d0fa3efec93b require explicit initialization of options;
wenzelm
parents: 45666
diff changeset
    89
48992
0518bf89c777 renamed Position.str_of to Position.here;
wenzelm
parents: 48920
diff changeset
    90
  /* here: inlined formal markup */
0518bf89c777 renamed Position.str_of to Position.here;
wenzelm
parents: 48920
diff changeset
    91
0518bf89c777 renamed Position.str_of to Position.here;
wenzelm
parents: 48920
diff changeset
    92
  def here(pos: T): String =
48920
9f84d872feba tuned signature;
wenzelm
parents: 48548
diff changeset
    93
    (Line.unapply(pos), File.unapply(pos)) match {
48370
d0fa3efec93b require explicit initialization of options;
wenzelm
parents: 45666
diff changeset
    94
      case (Some(i), None) => " (line " + i.toString + ")"
d0fa3efec93b require explicit initialization of options;
wenzelm
parents: 45666
diff changeset
    95
      case (Some(i), Some(name)) => " (line " + i.toString + " of " + quote(name) + ")"
d0fa3efec93b require explicit initialization of options;
wenzelm
parents: 45666
diff changeset
    96
      case (None, Some(name)) => " (file " + quote(name) + ")"
d0fa3efec93b require explicit initialization of options;
wenzelm
parents: 45666
diff changeset
    97
      case _ => ""
d0fa3efec93b require explicit initialization of options;
wenzelm
parents: 45666
diff changeset
    98
    }
27968
85b5f024d94b Position properties.
wenzelm
parents:
diff changeset
    99
}