src/Pure/General/position.ML
author wenzelm
Wed Jan 16 16:26:36 2013 +0100 (2013-01-16)
changeset 50911 ee7fe4230642
parent 50254 935ac0ad7e83
child 54038 f522477d671d
permissions -rw-r--r--
more explicit treatment of (optional) exception properties, notably for "serial" -- avoid conflict with startPosition = offset;
wenzelm@6118
     1
(*  Title:      Pure/General/position.ML
wenzelm@5010
     2
    Author:     Markus Wenzel, TU Muenchen
wenzelm@5010
     3
wenzelm@29307
     4
Source positions: counting Isabelle symbols, starting from 1.
wenzelm@5010
     5
*)
wenzelm@5010
     6
wenzelm@5010
     7
signature POSITION =
wenzelm@5010
     8
sig
wenzelm@41484
     9
  eqtype T
wenzelm@43710
    10
  val make: {line: int, offset: int, end_offset: int, props: Properties.T} -> T
wenzelm@43710
    11
  val dest: T -> {line: int, offset: int, end_offset: int, props: Properties.T}
wenzelm@23673
    12
  val line_of: T -> int option
wenzelm@27795
    13
  val offset_of: T -> int option
wenzelm@41484
    14
  val end_offset_of: T -> int option
wenzelm@23673
    15
  val file_of: T -> string option
wenzelm@27796
    16
  val advance: Symbol.symbol -> T -> T
wenzelm@27796
    17
  val distance_of: T -> T -> int
wenzelm@5010
    18
  val none: T
wenzelm@27777
    19
  val start: T
wenzelm@31435
    20
  val file_name: string -> Properties.T
wenzelm@44200
    21
  val file_only: string -> T
wenzelm@27777
    22
  val file: string -> T
wenzelm@5010
    23
  val line: int -> T
wenzelm@27777
    24
  val line_file: int -> string -> T
wenzelm@29307
    25
  val id: string -> T
wenzelm@32573
    26
  val id_only: string -> T
wenzelm@27426
    27
  val get_id: T -> string option
wenzelm@27426
    28
  val put_id: string -> T -> T
wenzelm@50911
    29
  val parse_id: T -> int option
wenzelm@28017
    30
  val of_properties: Properties.T -> T
wenzelm@28017
    31
  val properties_of: T -> Properties.T
wenzelm@42327
    32
  val def_properties_of: T -> Properties.T
wenzelm@45412
    33
  val entity_properties_of: bool -> serial -> T -> Properties.T
wenzelm@28017
    34
  val default_properties: T -> Properties.T -> Properties.T
wenzelm@39440
    35
  val markup: T -> Markup.T -> Markup.T
wenzelm@41504
    36
  val is_reported: T -> bool
wenzelm@39507
    37
  val reported_text: T -> Markup.T -> string -> string
wenzelm@39507
    38
  val report_text: T -> Markup.T -> string -> unit
wenzelm@39507
    39
  val report: T -> Markup.T -> unit
wenzelm@44736
    40
  type report = T * Markup.T
wenzelm@48767
    41
  type report_text = report * string
wenzelm@48767
    42
  val reports_text: report_text list -> unit
wenzelm@44736
    43
  val reports: report list -> unit
wenzelm@44736
    44
  val store_reports: report list Unsynchronized.ref -> T list -> ('a -> Markup.T list) -> 'a -> unit
wenzelm@48992
    45
  val here: T -> string
wenzelm@49691
    46
  val here_list: T list -> string
wenzelm@27764
    47
  type range = T * T
wenzelm@27796
    48
  val no_range: range
wenzelm@41484
    49
  val set_range: range -> T
wenzelm@27777
    50
  val reset_range: T -> T
wenzelm@27764
    51
  val range: T -> T -> range
wenzelm@25817
    52
  val thread_data: unit -> T
wenzelm@25817
    53
  val setmp_thread_data: T -> ('a -> 'b) -> 'a -> 'b
wenzelm@49528
    54
  val default: T -> bool * T
wenzelm@5010
    55
end;
wenzelm@5010
    56
wenzelm@5010
    57
structure Position: POSITION =
wenzelm@5010
    58
struct
wenzelm@5010
    59
wenzelm@5010
    60
(* datatype position *)
wenzelm@5010
    61
wenzelm@43710
    62
datatype T = Pos of (int * int * int) * Properties.T;
wenzelm@41484
    63
wenzelm@41484
    64
fun norm_props (props: Properties.T) =
wenzelm@45666
    65
  maps (fn a => the_list (find_first (fn (b, _) => a = b) props))
wenzelm@50201
    66
    Markup.position_properties';
wenzelm@41484
    67
wenzelm@43710
    68
fun make {line = i, offset = j, end_offset = k, props} = Pos ((i, j, k), norm_props props);
wenzelm@43710
    69
fun dest (Pos ((i, j, k), props)) = {line = i, offset = j, end_offset = k, props = props};
wenzelm@27777
    70
wenzelm@27795
    71
fun valid (i: int) = i > 0;
wenzelm@27795
    72
fun if_valid i i' = if valid i then i' else i;
wenzelm@27795
    73
wenzelm@27777
    74
wenzelm@27796
    75
(* fields *)
wenzelm@27796
    76
wenzelm@43710
    77
fun line_of (Pos ((i, _, _), _)) = if valid i then SOME i else NONE;
wenzelm@43710
    78
fun offset_of (Pos ((_, j, _), _)) = if valid j then SOME j else NONE;
wenzelm@43710
    79
fun end_offset_of (Pos ((_, _, k), _)) = if valid k then SOME k else NONE;
wenzelm@27796
    80
wenzelm@50201
    81
fun file_of (Pos (_, props)) = Properties.get props Markup.fileN;
wenzelm@27796
    82
wenzelm@27796
    83
wenzelm@27777
    84
(* advance *)
wenzelm@26003
    85
wenzelm@43710
    86
fun advance_count "\n" (i: int, j: int, k: int) =
wenzelm@43710
    87
      (if_valid i (i + 1), if_valid j (j + 1), k)
wenzelm@43710
    88
  | advance_count s (i, j, k) =
wenzelm@43710
    89
      if Symbol.is_regular s then (i, if_valid j (j + 1), k)
wenzelm@43710
    90
      else (i, j, k);
wenzelm@5010
    91
wenzelm@43710
    92
fun invalid_count (i, j, _: int) =
wenzelm@43710
    93
  not (valid i orelse valid j);
wenzelm@27795
    94
wenzelm@27795
    95
fun advance sym (pos as (Pos (count, props))) =
wenzelm@27795
    96
  if invalid_count count then pos else Pos (advance_count sym count, props);
wenzelm@27777
    97
wenzelm@27777
    98
wenzelm@27796
    99
(* distance of adjacent positions *)
wenzelm@27777
   100
wenzelm@43710
   101
fun distance_of (Pos ((_, j, _), _)) (Pos ((_, j', _), _)) =
wenzelm@27796
   102
  if valid j andalso valid j' then j' - j
wenzelm@27796
   103
  else 0;
wenzelm@26882
   104
wenzelm@5010
   105
wenzelm@27777
   106
(* make position *)
wenzelm@27777
   107
wenzelm@43710
   108
val none = Pos ((0, 0, 0), []);
wenzelm@43710
   109
val start = Pos ((1, 1, 0), []);
wenzelm@27744
   110
wenzelm@29307
   111
wenzelm@27796
   112
fun file_name "" = []
wenzelm@50201
   113
  | file_name name = [(Markup.fileN, name)];
wenzelm@27796
   114
wenzelm@44200
   115
fun file_only name = Pos ((0, 0, 0), file_name name);
wenzelm@43710
   116
fun file name = Pos ((1, 1, 0), file_name name);
wenzelm@27744
   117
wenzelm@43710
   118
fun line_file i name = Pos ((i, 1, 0), file_name name);
wenzelm@27795
   119
fun line i = line_file i "";
wenzelm@5010
   120
wenzelm@50201
   121
fun id id = Pos ((0, 1, 0), [(Markup.idN, id)]);
wenzelm@50201
   122
fun id_only id = Pos ((0, 0, 0), [(Markup.idN, id)]);
aspinall@22158
   123
wenzelm@50201
   124
fun get_id (Pos (_, props)) = Properties.get props Markup.idN;
wenzelm@50201
   125
fun put_id id (Pos (count, props)) = Pos (count, Properties.put (Markup.idN, id) props);
wenzelm@27426
   126
wenzelm@50911
   127
fun parse_id pos = Option.map Markup.parse_int (get_id pos);
wenzelm@50911
   128
wenzelm@29307
   129
wenzelm@29307
   130
(* markup properties *)
wenzelm@29307
   131
wenzelm@25817
   132
fun of_properties props =
wenzelm@23627
   133
  let
wenzelm@27795
   134
    fun get name =
wenzelm@28017
   135
      (case Properties.get props name of
wenzelm@27795
   136
        NONE => 0
wenzelm@50254
   137
      | SOME s => Markup.parse_int s);
wenzelm@41484
   138
  in
wenzelm@50201
   139
    make {line = get Markup.lineN, offset = get Markup.offsetN,
wenzelm@50201
   140
      end_offset = get Markup.end_offsetN, props = props}
wenzelm@41484
   141
  end;
wenzelm@41484
   142
wenzelm@26003
   143
wenzelm@50254
   144
fun value k i = if valid i then [(k, Markup.print_int i)] else [];
wenzelm@41484
   145
wenzelm@43710
   146
fun properties_of (Pos ((i, j, k), props)) =
wenzelm@50201
   147
  value Markup.lineN i @ value Markup.offsetN j @ value Markup.end_offsetN k @ props;
wenzelm@26003
   148
wenzelm@42327
   149
val def_properties_of = properties_of #> (map (fn (x, y) => ("def_" ^ x, y)));
wenzelm@42327
   150
wenzelm@45412
   151
fun entity_properties_of def id pos =
wenzelm@50254
   152
  if def then (Markup.defN, Markup.print_int id) :: properties_of pos
wenzelm@50254
   153
  else (Markup.refN, Markup.print_int id) :: def_properties_of pos;
wenzelm@45412
   154
wenzelm@26052
   155
fun default_properties default props =
wenzelm@50201
   156
  if exists (member (op =) Markup.position_properties o #1) props then props
wenzelm@26052
   157
  else properties_of default @ props;
wenzelm@26052
   158
wenzelm@39440
   159
val markup = Markup.properties o properties_of;
wenzelm@39440
   160
wenzelm@39440
   161
wenzelm@39440
   162
(* reports *)
wenzelm@38887
   163
wenzelm@41504
   164
fun is_reported pos = is_some (offset_of pos) andalso is_some (get_id pos);
wenzelm@30669
   165
wenzelm@41504
   166
fun reported_text pos m txt = if is_reported pos then Markup.markup (markup pos m) txt else "";
wenzelm@39507
   167
fun report_text pos markup txt = Output.report (reported_text pos markup txt);
wenzelm@39507
   168
fun report pos markup = report_text pos markup "";
wenzelm@27764
   169
wenzelm@44736
   170
type report = T * Markup.T;
wenzelm@48767
   171
type report_text = report * string;
wenzelm@44736
   172
wenzelm@48767
   173
val reports_text =
wenzelm@48767
   174
  map (fn ((pos, m), txt) => if is_reported pos then Markup.markup (markup pos m) txt else "")
wenzelm@44736
   175
  #> implode #> Output.report;
wenzelm@42204
   176
wenzelm@48767
   177
val reports = map (rpair "") #> reports_text;
wenzelm@48767
   178
wenzelm@44735
   179
fun store_reports _ [] _ _ = ()
wenzelm@44736
   180
  | store_reports (r: report list Unsynchronized.ref) ps markup x =
wenzelm@42204
   181
      let val ms = markup x
wenzelm@42204
   182
      in Unsynchronized.change r (fold (fn p => fold (fn m => cons (p, m)) ms) ps) end;
wenzelm@42204
   183
wenzelm@25817
   184
wenzelm@48992
   185
(* here: inlined formal markup *)
wenzelm@26003
   186
wenzelm@48992
   187
fun here pos =
wenzelm@26003
   188
  let
wenzelm@26003
   189
    val props = properties_of pos;
wenzelm@26003
   190
    val s =
wenzelm@26003
   191
      (case (line_of pos, file_of pos) of
wenzelm@50254
   192
        (SOME i, NONE) => "(line " ^ Markup.print_int i ^ ")"
wenzelm@50254
   193
      | (SOME i, SOME name) => "(line " ^ Markup.print_int i ^ " of " ^ quote name ^ ")"
wenzelm@44224
   194
      | (NONE, SOME name) => "(file " ^ quote name ^ ")"
wenzelm@26003
   195
      | _ => "");
wenzelm@26003
   196
  in
wenzelm@26003
   197
    if null props then ""
wenzelm@50201
   198
    else (if s = "" then "" else " ") ^ Markup.markup (Markup.properties props Markup.position) s
wenzelm@26003
   199
  end;
wenzelm@25817
   200
wenzelm@49691
   201
val here_list = space_implode " " o map here;
wenzelm@49691
   202
wenzelm@23627
   203
wenzelm@27736
   204
(* range *)
wenzelm@27736
   205
wenzelm@27736
   206
type range = T * T;
wenzelm@27736
   207
wenzelm@27796
   208
val no_range = (none, none);
wenzelm@27796
   209
wenzelm@43710
   210
fun set_range (Pos ((i, j, _), props), Pos ((_, j', _), _)) = Pos ((i, j, j'), props);
wenzelm@43710
   211
fun reset_range (Pos ((i, j, _), props)) = Pos ((i, j, 0), props);
wenzelm@27777
   212
wenzelm@41484
   213
fun range pos pos' = (set_range (pos, pos'), pos');
wenzelm@27741
   214
wenzelm@27764
   215
wenzelm@27764
   216
(* thread data *)
wenzelm@27764
   217
wenzelm@27764
   218
local val tag = Universal.tag () : T Universal.tag in
wenzelm@27741
   219
wenzelm@28122
   220
fun thread_data () = the_default none (Thread.getLocal tag);
wenzelm@27764
   221
wenzelm@37043
   222
fun setmp_thread_data pos = Library.setmp_thread_data tag (thread_data ()) pos;
wenzelm@27764
   223
wenzelm@5010
   224
end;
wenzelm@27764
   225
wenzelm@33097
   226
fun default pos =
wenzelm@49528
   227
  if pos = none then (false, thread_data ())
wenzelm@49528
   228
  else (true, pos);
wenzelm@33097
   229
wenzelm@27764
   230
end;