src/Pure/General/position.scala
author wenzelm
Fri, 16 Mar 2018 17:16:09 +0100
changeset 67882 7eb4c966e156
parent 65402 37d3657e8513
child 68287 2ae74a278c10
permissions -rw-r--r--
JSON representation for Position.T;
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
55490
9b0fb0e2c9f5 updated thy_info.dependencies;
wenzelm
parents: 55429
diff changeset
    17
  val none: T = Nil
9b0fb0e2c9f5 updated thy_info.dependencies;
wenzelm
parents: 55429
diff changeset
    18
50201
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49419
diff changeset
    19
  val Line = new Properties.Int(Markup.LINE)
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49419
diff changeset
    20
  val Offset = new Properties.Int(Markup.OFFSET)
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49419
diff changeset
    21
  val End_Offset = new Properties.Int(Markup.END_OFFSET)
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49419
diff changeset
    22
  val File = new Properties.String(Markup.FILE)
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49419
diff changeset
    23
  val Id = new Properties.Long(Markup.ID)
59706
bf6ca55aae13 proper command id for inlined errors, which is important for Command.State.accumulate;
wenzelm
parents: 59671
diff changeset
    24
  val Id_String = new Properties.String(Markup.ID)
31705
0c83e3e75fcf replaced java Properties by pure property lists;
wenzelm
parents: 29140
diff changeset
    25
50201
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49419
diff changeset
    26
  val Def_Line = new Properties.Int(Markup.DEF_LINE)
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49419
diff changeset
    27
  val Def_Offset = new Properties.Int(Markup.DEF_OFFSET)
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49419
diff changeset
    28
  val Def_End_Offset = new Properties.Int(Markup.DEF_END_OFFSET)
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49419
diff changeset
    29
  val Def_File = new Properties.String(Markup.DEF_FILE)
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49419
diff changeset
    30
  val Def_Id = new Properties.Long(Markup.DEF_ID)
49419
e2726211f834 pass base_snapshot to enable hyperlinks into other nodes;
wenzelm
parents: 48992
diff changeset
    31
48920
9f84d872feba tuned signature;
wenzelm
parents: 48548
diff changeset
    32
  object Line_File
9f84d872feba tuned signature;
wenzelm
parents: 48548
diff changeset
    33
  {
56464
555f4be59be6 more precise token positions;
wenzelm
parents: 56462
diff changeset
    34
    def apply(line: Int, file: String): T =
555f4be59be6 more precise token positions;
wenzelm
parents: 56462
diff changeset
    35
      (if (line > 0) Line(line) else Nil) :::
555f4be59be6 more precise token positions;
wenzelm
parents: 56462
diff changeset
    36
      (if (file != "") File(file) else Nil)
555f4be59be6 more precise token positions;
wenzelm
parents: 56462
diff changeset
    37
48920
9f84d872feba tuned signature;
wenzelm
parents: 48548
diff changeset
    38
    def unapply(pos: T): Option[(Int, String)] =
9f84d872feba tuned signature;
wenzelm
parents: 48548
diff changeset
    39
      (pos, pos) match {
9f84d872feba tuned signature;
wenzelm
parents: 48548
diff changeset
    40
        case (Line(i), File(name)) => Some((i, name))
9f84d872feba tuned signature;
wenzelm
parents: 48548
diff changeset
    41
        case (_, File(name)) => Some((1, name))
9f84d872feba tuned signature;
wenzelm
parents: 48548
diff changeset
    42
        case _ => None
9f84d872feba tuned signature;
wenzelm
parents: 48548
diff changeset
    43
      }
9f84d872feba tuned signature;
wenzelm
parents: 48548
diff changeset
    44
  }
9f84d872feba tuned signature;
wenzelm
parents: 48548
diff changeset
    45
49419
e2726211f834 pass base_snapshot to enable hyperlinks into other nodes;
wenzelm
parents: 48992
diff changeset
    46
  object Def_Line_File
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
    def unapply(pos: T): Option[(Int, String)] =
e2726211f834 pass base_snapshot to enable hyperlinks into other nodes;
wenzelm
parents: 48992
diff changeset
    49
      (pos, pos) match {
e2726211f834 pass base_snapshot to enable hyperlinks into other nodes;
wenzelm
parents: 48992
diff changeset
    50
        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
    51
        case (_, Def_File(name)) => Some((1, name))
e2726211f834 pass base_snapshot to enable hyperlinks into other nodes;
wenzelm
parents: 48992
diff changeset
    52
        case _ => None
e2726211f834 pass base_snapshot to enable hyperlinks into other nodes;
wenzelm
parents: 48992
diff changeset
    53
      }
e2726211f834 pass base_snapshot to enable hyperlinks into other nodes;
wenzelm
parents: 48992
diff changeset
    54
  }
e2726211f834 pass base_snapshot to enable hyperlinks into other nodes;
wenzelm
parents: 48992
diff changeset
    55
38722
ba31936497c2 organized markup properties via apply/unapply patterns;
wenzelm
parents: 38568
diff changeset
    56
  object Range
ba31936497c2 organized markup properties via apply/unapply patterns;
wenzelm
parents: 38568
diff changeset
    57
  {
57910
a50837b637dc maintain Command_Range position as in ML;
wenzelm
parents: 56746
diff changeset
    58
    def apply(range: Symbol.Range): T = Offset(range.start) ::: End_Offset(range.stop)
55884
f2c0eaedd579 tuned signature -- emphasize symbol positions (prover) vs. decoded text offsets (editor);
wenzelm
parents: 55555
diff changeset
    59
    def unapply(pos: T): Option[Symbol.Range] =
48920
9f84d872feba tuned signature;
wenzelm
parents: 48548
diff changeset
    60
      (pos, pos) match {
9f84d872feba tuned signature;
wenzelm
parents: 48548
diff changeset
    61
        case (Offset(start), End_Offset(stop)) if start <= stop => Some(Text.Range(start, stop))
9f84d872feba tuned signature;
wenzelm
parents: 48548
diff changeset
    62
        case (Offset(start), _) => Some(Text.Range(start, start + 1))
9f84d872feba tuned signature;
wenzelm
parents: 48548
diff changeset
    63
        case _ => None
9f84d872feba tuned signature;
wenzelm
parents: 48548
diff changeset
    64
      }
9f84d872feba tuned signature;
wenzelm
parents: 48548
diff changeset
    65
  }
9f84d872feba tuned signature;
wenzelm
parents: 48548
diff changeset
    66
64662
wenzelm
parents: 59707
diff changeset
    67
  object Item_Id
48920
9f84d872feba tuned signature;
wenzelm
parents: 48548
diff changeset
    68
  {
64667
cdb0d559a24b full range for Position.Item;
wenzelm
parents: 64662
diff changeset
    69
    def unapply(pos: T): Option[(Long, Symbol.Range)] =
57931
wenzelm
parents: 57911
diff changeset
    70
      pos match {
64667
cdb0d559a24b full range for Position.Item;
wenzelm
parents: 64662
diff changeset
    71
        case Id(id) =>
cdb0d559a24b full range for Position.Item;
wenzelm
parents: 64662
diff changeset
    72
          val offset = Offset.unapply(pos) getOrElse 0
cdb0d559a24b full range for Position.Item;
wenzelm
parents: 64662
diff changeset
    73
          val end_offset = End_Offset.unapply(pos) getOrElse (offset + 1)
cdb0d559a24b full range for Position.Item;
wenzelm
parents: 64662
diff changeset
    74
          Some((id, Text.Range(offset, end_offset)))
38722
ba31936497c2 organized markup properties via apply/unapply patterns;
wenzelm
parents: 38568
diff changeset
    75
        case _ => None
ba31936497c2 organized markup properties via apply/unapply patterns;
wenzelm
parents: 38568
diff changeset
    76
      }
ba31936497c2 organized markup properties via apply/unapply patterns;
wenzelm
parents: 38568
diff changeset
    77
  }
38872
26c505765024 Command.results: ordered by serial number;
wenzelm
parents: 38722
diff changeset
    78
64662
wenzelm
parents: 59707
diff changeset
    79
  object Item_Def_Id
49419
e2726211f834 pass base_snapshot to enable hyperlinks into other nodes;
wenzelm
parents: 48992
diff changeset
    80
  {
64667
cdb0d559a24b full range for Position.Item;
wenzelm
parents: 64662
diff changeset
    81
    def unapply(pos: T): Option[(Long, Symbol.Range)] =
57931
wenzelm
parents: 57911
diff changeset
    82
      pos match {
64667
cdb0d559a24b full range for Position.Item;
wenzelm
parents: 64662
diff changeset
    83
        case Def_Id(id) =>
cdb0d559a24b full range for Position.Item;
wenzelm
parents: 64662
diff changeset
    84
          val offset = Def_Offset.unapply(pos) getOrElse 0
cdb0d559a24b full range for Position.Item;
wenzelm
parents: 64662
diff changeset
    85
          val end_offset = Def_End_Offset.unapply(pos) getOrElse (offset + 1)
cdb0d559a24b full range for Position.Item;
wenzelm
parents: 64662
diff changeset
    86
          Some((id, Text.Range(offset, end_offset)))
49419
e2726211f834 pass base_snapshot to enable hyperlinks into other nodes;
wenzelm
parents: 48992
diff changeset
    87
        case _ => None
e2726211f834 pass base_snapshot to enable hyperlinks into other nodes;
wenzelm
parents: 48992
diff changeset
    88
      }
e2726211f834 pass base_snapshot to enable hyperlinks into other nodes;
wenzelm
parents: 48992
diff changeset
    89
  }
e2726211f834 pass base_snapshot to enable hyperlinks into other nodes;
wenzelm
parents: 48992
diff changeset
    90
64662
wenzelm
parents: 59707
diff changeset
    91
  object Item_File
wenzelm
parents: 59707
diff changeset
    92
  {
64667
cdb0d559a24b full range for Position.Item;
wenzelm
parents: 64662
diff changeset
    93
    def unapply(pos: T): Option[(String, Int, Symbol.Range)] =
64662
wenzelm
parents: 59707
diff changeset
    94
      pos match {
wenzelm
parents: 59707
diff changeset
    95
        case Line_File(line, name) =>
64667
cdb0d559a24b full range for Position.Item;
wenzelm
parents: 64662
diff changeset
    96
          val offset = Offset.unapply(pos) getOrElse 0
cdb0d559a24b full range for Position.Item;
wenzelm
parents: 64662
diff changeset
    97
          val end_offset = End_Offset.unapply(pos) getOrElse (offset + 1)
cdb0d559a24b full range for Position.Item;
wenzelm
parents: 64662
diff changeset
    98
          Some((name, line, Text.Range(offset, end_offset)))
64662
wenzelm
parents: 59707
diff changeset
    99
        case _ => None
wenzelm
parents: 59707
diff changeset
   100
      }
wenzelm
parents: 59707
diff changeset
   101
  }
wenzelm
parents: 59707
diff changeset
   102
wenzelm
parents: 59707
diff changeset
   103
  object Item_Def_File
wenzelm
parents: 59707
diff changeset
   104
  {
64667
cdb0d559a24b full range for Position.Item;
wenzelm
parents: 64662
diff changeset
   105
    def unapply(pos: T): Option[(String, Int, Symbol.Range)] =
64662
wenzelm
parents: 59707
diff changeset
   106
      pos match {
wenzelm
parents: 59707
diff changeset
   107
        case Def_Line_File(line, name) =>
64667
cdb0d559a24b full range for Position.Item;
wenzelm
parents: 64662
diff changeset
   108
          val offset = Def_Offset.unapply(pos) getOrElse 0
cdb0d559a24b full range for Position.Item;
wenzelm
parents: 64662
diff changeset
   109
          val end_offset = Def_End_Offset.unapply(pos) getOrElse (offset + 1)
cdb0d559a24b full range for Position.Item;
wenzelm
parents: 64662
diff changeset
   110
          Some((name, line, Text.Range(offset, end_offset)))
64662
wenzelm
parents: 59707
diff changeset
   111
        case _ => None
wenzelm
parents: 59707
diff changeset
   112
      }
wenzelm
parents: 59707
diff changeset
   113
  }
wenzelm
parents: 59707
diff changeset
   114
57911
dcb758188aa6 clarified Position.Identified: do not require range from prover, default to command position;
wenzelm
parents: 57910
diff changeset
   115
  object Identified
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
   116
  {
57911
dcb758188aa6 clarified Position.Identified: do not require range from prover, default to command position;
wenzelm
parents: 57910
diff changeset
   117
    def unapply(pos: T): Option[(Long, Symbol.Text_Chunk.Name)] =
dcb758188aa6 clarified Position.Identified: do not require range from prover, default to command position;
wenzelm
parents: 57910
diff changeset
   118
      pos match {
dcb758188aa6 clarified Position.Identified: do not require range from prover, default to command position;
wenzelm
parents: 57910
diff changeset
   119
        case Id(id) =>
56462
b64b0cb845fe more explicit Command.Chunk types, less ooddities;
wenzelm
parents: 55884
diff changeset
   120
          val chunk_name =
b64b0cb845fe more explicit Command.Chunk types, less ooddities;
wenzelm
parents: 55884
diff changeset
   121
            pos match {
56746
d37a5d09a277 tuned signature;
wenzelm
parents: 56532
diff changeset
   122
              case File(name) => Symbol.Text_Chunk.File(name)
d37a5d09a277 tuned signature;
wenzelm
parents: 56532
diff changeset
   123
              case _ => Symbol.Text_Chunk.Default
56462
b64b0cb845fe more explicit Command.Chunk types, less ooddities;
wenzelm
parents: 55884
diff changeset
   124
            }
57911
dcb758188aa6 clarified Position.Identified: do not require range from prover, default to command position;
wenzelm
parents: 57910
diff changeset
   125
          Some((id, chunk_name))
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
   126
        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
   127
      }
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
   128
  }
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
   129
50201
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49419
diff changeset
   130
  def purge(props: T): T = props.filterNot(p => Markup.POSITION_PROPERTIES(p._1))
48370
d0fa3efec93b require explicit initialization of options;
wenzelm
parents: 45666
diff changeset
   131
d0fa3efec93b require explicit initialization of options;
wenzelm
parents: 45666
diff changeset
   132
56532
3da244bc02bd tuned message, to accommodate extra brackets produced by Scala parsers;
wenzelm
parents: 56473
diff changeset
   133
  /* here: user output */
48992
0518bf89c777 renamed Position.str_of to Position.here;
wenzelm
parents: 48920
diff changeset
   134
65402
37d3657e8513 proper default (amending 601866c61ded);
wenzelm
parents: 64728
diff changeset
   135
  def here(props: T, delimited: Boolean = true): String =
64728
601866c61ded more precise markup;
wenzelm
parents: 64667
diff changeset
   136
  {
601866c61ded more precise markup;
wenzelm
parents: 64667
diff changeset
   137
    val pos = props.filter(p => Markup.POSITION_PROPERTIES(p._1))
601866c61ded more precise markup;
wenzelm
parents: 64667
diff changeset
   138
    if (pos.isEmpty) ""
601866c61ded more precise markup;
wenzelm
parents: 64667
diff changeset
   139
    else {
601866c61ded more precise markup;
wenzelm
parents: 64667
diff changeset
   140
      val s0 =
601866c61ded more precise markup;
wenzelm
parents: 64667
diff changeset
   141
        (Line.unapply(pos), File.unapply(pos)) match {
601866c61ded more precise markup;
wenzelm
parents: 64667
diff changeset
   142
          case (Some(i), None) => "line " + i.toString
601866c61ded more precise markup;
wenzelm
parents: 64667
diff changeset
   143
          case (Some(i), Some(name)) => "line " + i.toString + " of " + quote(name)
601866c61ded more precise markup;
wenzelm
parents: 64667
diff changeset
   144
          case (None, Some(name)) => "file " + quote(name)
601866c61ded more precise markup;
wenzelm
parents: 64667
diff changeset
   145
          case _ => ""
601866c61ded more precise markup;
wenzelm
parents: 64667
diff changeset
   146
        }
601866c61ded more precise markup;
wenzelm
parents: 64667
diff changeset
   147
      val s = if (s0 == "") s0 else if (delimited) " (" + s0 + ")" else " " + s0
601866c61ded more precise markup;
wenzelm
parents: 64667
diff changeset
   148
      Markup(Markup.POSITION, pos).markup(s)
601866c61ded more precise markup;
wenzelm
parents: 64667
diff changeset
   149
    }
601866c61ded more precise markup;
wenzelm
parents: 64667
diff changeset
   150
  }
67882
7eb4c966e156 JSON representation for Position.T;
wenzelm
parents: 65402
diff changeset
   151
7eb4c966e156 JSON representation for Position.T;
wenzelm
parents: 65402
diff changeset
   152
7eb4c966e156 JSON representation for Position.T;
wenzelm
parents: 65402
diff changeset
   153
  /* JSON representation */
7eb4c966e156 JSON representation for Position.T;
wenzelm
parents: 65402
diff changeset
   154
7eb4c966e156 JSON representation for Position.T;
wenzelm
parents: 65402
diff changeset
   155
  object JSON
7eb4c966e156 JSON representation for Position.T;
wenzelm
parents: 65402
diff changeset
   156
  {
7eb4c966e156 JSON representation for Position.T;
wenzelm
parents: 65402
diff changeset
   157
    def apply(pos: T): isabelle.JSON.Object.T =
7eb4c966e156 JSON representation for Position.T;
wenzelm
parents: 65402
diff changeset
   158
      isabelle.JSON.Object.empty ++
7eb4c966e156 JSON representation for Position.T;
wenzelm
parents: 65402
diff changeset
   159
        Line.unapply(pos).map(Line.name -> _) ++
7eb4c966e156 JSON representation for Position.T;
wenzelm
parents: 65402
diff changeset
   160
        Offset.unapply(pos).map(Offset.name -> _) ++
7eb4c966e156 JSON representation for Position.T;
wenzelm
parents: 65402
diff changeset
   161
        End_Offset.unapply(pos).map(End_Offset.name -> _) ++
7eb4c966e156 JSON representation for Position.T;
wenzelm
parents: 65402
diff changeset
   162
        File.unapply(pos).map(File.name -> _) ++
7eb4c966e156 JSON representation for Position.T;
wenzelm
parents: 65402
diff changeset
   163
        Id.unapply(pos).map(Id.name -> _)
7eb4c966e156 JSON representation for Position.T;
wenzelm
parents: 65402
diff changeset
   164
7eb4c966e156 JSON representation for Position.T;
wenzelm
parents: 65402
diff changeset
   165
    def unapply(json: isabelle.JSON.T): Option[T] =
7eb4c966e156 JSON representation for Position.T;
wenzelm
parents: 65402
diff changeset
   166
      for {
7eb4c966e156 JSON representation for Position.T;
wenzelm
parents: 65402
diff changeset
   167
        line <- isabelle.JSON.int_default(json, Line.name)
7eb4c966e156 JSON representation for Position.T;
wenzelm
parents: 65402
diff changeset
   168
        offset <- isabelle.JSON.int_default(json, Offset.name)
7eb4c966e156 JSON representation for Position.T;
wenzelm
parents: 65402
diff changeset
   169
        end_offset <- isabelle.JSON.int_default(json, End_Offset.name)
7eb4c966e156 JSON representation for Position.T;
wenzelm
parents: 65402
diff changeset
   170
        file <- isabelle.JSON.string_default(json, File.name)
7eb4c966e156 JSON representation for Position.T;
wenzelm
parents: 65402
diff changeset
   171
        id <- isabelle.JSON.long_default(json, Id.name)
7eb4c966e156 JSON representation for Position.T;
wenzelm
parents: 65402
diff changeset
   172
      }
7eb4c966e156 JSON representation for Position.T;
wenzelm
parents: 65402
diff changeset
   173
      yield {
7eb4c966e156 JSON representation for Position.T;
wenzelm
parents: 65402
diff changeset
   174
        def defined(name: String): Boolean = isabelle.JSON.value(json, name).isDefined
7eb4c966e156 JSON representation for Position.T;
wenzelm
parents: 65402
diff changeset
   175
        (if (defined(Line.name)) Line(line) else Nil) :::
7eb4c966e156 JSON representation for Position.T;
wenzelm
parents: 65402
diff changeset
   176
        (if (defined(Offset.name)) Offset(offset) else Nil) :::
7eb4c966e156 JSON representation for Position.T;
wenzelm
parents: 65402
diff changeset
   177
        (if (defined(End_Offset.name)) End_Offset(end_offset) else Nil) :::
7eb4c966e156 JSON representation for Position.T;
wenzelm
parents: 65402
diff changeset
   178
        (if (defined(File.name)) File(file) else Nil) :::
7eb4c966e156 JSON representation for Position.T;
wenzelm
parents: 65402
diff changeset
   179
        (if (defined(Id.name)) Id(id) else Nil)
7eb4c966e156 JSON representation for Position.T;
wenzelm
parents: 65402
diff changeset
   180
      }
7eb4c966e156 JSON representation for Position.T;
wenzelm
parents: 65402
diff changeset
   181
  }
27968
85b5f024d94b Position properties.
wenzelm
parents:
diff changeset
   182
}