src/Pure/General/position.ML
author wenzelm
Wed Apr 06 16:33:33 2016 +0200 (2016-04-06)
changeset 62889 99c7f31615c2
parent 62803 5f73bf6ba98b
child 62929 b92565f98206
permissions -rw-r--r--
clarified modules;
tuned signature;
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@59085
    17
  val advance_offset: int -> T -> T
wenzelm@27796
    18
  val distance_of: T -> T -> int
wenzelm@5010
    19
  val none: T
wenzelm@27777
    20
  val start: T
wenzelm@31435
    21
  val file_name: string -> Properties.T
wenzelm@44200
    22
  val file_only: string -> T
wenzelm@27777
    23
  val file: string -> T
wenzelm@56437
    24
  val line_file_only: int -> string -> T
wenzelm@56437
    25
  val line_file: int -> string -> T
wenzelm@5010
    26
  val line: int -> T
wenzelm@29307
    27
  val id: string -> T
wenzelm@32573
    28
  val id_only: string -> T
wenzelm@27426
    29
  val get_id: T -> string option
wenzelm@27426
    30
  val put_id: string -> T -> T
wenzelm@50911
    31
  val parse_id: T -> int option
wenzelm@28017
    32
  val of_properties: Properties.T -> T
wenzelm@28017
    33
  val properties_of: T -> Properties.T
wenzelm@42327
    34
  val def_properties_of: T -> Properties.T
wenzelm@45412
    35
  val entity_properties_of: bool -> serial -> T -> Properties.T
wenzelm@28017
    36
  val default_properties: T -> Properties.T -> Properties.T
wenzelm@39440
    37
  val markup: T -> Markup.T -> Markup.T
wenzelm@41504
    38
  val is_reported: T -> bool
wenzelm@56459
    39
  val is_reported_range: T -> bool
wenzelm@39507
    40
  val reported_text: T -> Markup.T -> string -> string
wenzelm@39507
    41
  val report_text: T -> Markup.T -> string -> unit
wenzelm@39507
    42
  val report: T -> Markup.T -> unit
wenzelm@44736
    43
  type report = T * Markup.T
wenzelm@48767
    44
  type report_text = report * string
wenzelm@48767
    45
  val reports_text: report_text list -> unit
wenzelm@44736
    46
  val reports: report list -> unit
wenzelm@55922
    47
  val store_reports: report_text list Unsynchronized.ref ->
wenzelm@55922
    48
    T list -> ('a -> Markup.T list) -> 'a -> unit
wenzelm@55959
    49
  val append_reports: report_text list Unsynchronized.ref -> report list -> unit
wenzelm@48992
    50
  val here: T -> string
wenzelm@49691
    51
  val here_list: T list -> string
wenzelm@27764
    52
  type range = T * T
wenzelm@27796
    53
  val no_range: range
wenzelm@62800
    54
  val no_range_position: T -> T
wenzelm@62797
    55
  val range_position: range -> T
wenzelm@62797
    56
  val range: T * T -> range
wenzelm@58978
    57
  val range_of_properties: Properties.T -> range
wenzelm@58978
    58
  val properties_of_range: range -> Properties.T
wenzelm@25817
    59
  val thread_data: unit -> T
wenzelm@25817
    60
  val setmp_thread_data: T -> ('a -> 'b) -> 'a -> 'b
wenzelm@49528
    61
  val default: T -> bool * T
wenzelm@5010
    62
end;
wenzelm@5010
    63
wenzelm@5010
    64
structure Position: POSITION =
wenzelm@5010
    65
struct
wenzelm@5010
    66
wenzelm@5010
    67
(* datatype position *)
wenzelm@5010
    68
wenzelm@43710
    69
datatype T = Pos of (int * int * int) * Properties.T;
wenzelm@41484
    70
wenzelm@41484
    71
fun norm_props (props: Properties.T) =
wenzelm@45666
    72
  maps (fn a => the_list (find_first (fn (b, _) => a = b) props))
wenzelm@50201
    73
    Markup.position_properties';
wenzelm@41484
    74
wenzelm@43710
    75
fun make {line = i, offset = j, end_offset = k, props} = Pos ((i, j, k), norm_props props);
wenzelm@43710
    76
fun dest (Pos ((i, j, k), props)) = {line = i, offset = j, end_offset = k, props = props};
wenzelm@27777
    77
wenzelm@27795
    78
fun valid (i: int) = i > 0;
wenzelm@27795
    79
fun if_valid i i' = if valid i then i' else i;
wenzelm@27795
    80
wenzelm@27777
    81
wenzelm@27796
    82
(* fields *)
wenzelm@27796
    83
wenzelm@43710
    84
fun line_of (Pos ((i, _, _), _)) = if valid i then SOME i else NONE;
wenzelm@43710
    85
fun offset_of (Pos ((_, j, _), _)) = if valid j then SOME j else NONE;
wenzelm@43710
    86
fun end_offset_of (Pos ((_, _, k), _)) = if valid k then SOME k else NONE;
wenzelm@27796
    87
wenzelm@50201
    88
fun file_of (Pos (_, props)) = Properties.get props Markup.fileN;
wenzelm@27796
    89
wenzelm@27796
    90
wenzelm@27777
    91
(* advance *)
wenzelm@26003
    92
wenzelm@43710
    93
fun advance_count "\n" (i: int, j: int, k: int) =
wenzelm@43710
    94
      (if_valid i (i + 1), if_valid j (j + 1), k)
wenzelm@43710
    95
  | advance_count s (i, j, k) =
wenzelm@58854
    96
      if Symbol.not_eof s then (i, if_valid j (j + 1), k)
wenzelm@43710
    97
      else (i, j, k);
wenzelm@5010
    98
wenzelm@43710
    99
fun invalid_count (i, j, _: int) =
wenzelm@43710
   100
  not (valid i orelse valid j);
wenzelm@27795
   101
wenzelm@27795
   102
fun advance sym (pos as (Pos (count, props))) =
wenzelm@27795
   103
  if invalid_count count then pos else Pos (advance_count sym count, props);
wenzelm@27777
   104
wenzelm@59085
   105
fun advance_offset offset (pos as (Pos (count as (i, j, k), props))) =
wenzelm@59085
   106
  if invalid_count count then pos
wenzelm@59085
   107
  else if valid i then raise Fail "Illegal line position"
wenzelm@59085
   108
  else Pos ((i, if_valid j (j + offset), k), props);
wenzelm@59085
   109
wenzelm@27777
   110
wenzelm@27796
   111
(* distance of adjacent positions *)
wenzelm@27777
   112
wenzelm@43710
   113
fun distance_of (Pos ((_, j, _), _)) (Pos ((_, j', _), _)) =
wenzelm@27796
   114
  if valid j andalso valid j' then j' - j
wenzelm@27796
   115
  else 0;
wenzelm@26882
   116
wenzelm@5010
   117
wenzelm@27777
   118
(* make position *)
wenzelm@27777
   119
wenzelm@43710
   120
val none = Pos ((0, 0, 0), []);
wenzelm@43710
   121
val start = Pos ((1, 1, 0), []);
wenzelm@27744
   122
wenzelm@29307
   123
wenzelm@27796
   124
fun file_name "" = []
wenzelm@50201
   125
  | file_name name = [(Markup.fileN, name)];
wenzelm@27796
   126
wenzelm@44200
   127
fun file_only name = Pos ((0, 0, 0), file_name name);
wenzelm@43710
   128
fun file name = Pos ((1, 1, 0), file_name name);
wenzelm@27744
   129
wenzelm@56437
   130
fun line_file_only i name = Pos ((i, 0, 0), file_name name);
wenzelm@43710
   131
fun line_file i name = Pos ((i, 1, 0), file_name name);
wenzelm@27795
   132
fun line i = line_file i "";
wenzelm@5010
   133
wenzelm@50201
   134
fun id id = Pos ((0, 1, 0), [(Markup.idN, id)]);
wenzelm@50201
   135
fun id_only id = Pos ((0, 0, 0), [(Markup.idN, id)]);
aspinall@22158
   136
wenzelm@50201
   137
fun get_id (Pos (_, props)) = Properties.get props Markup.idN;
wenzelm@62750
   138
fun put_id id (Pos (count, props)) = Pos (count, norm_props (Properties.put (Markup.idN, id) props));
wenzelm@27426
   139
wenzelm@50911
   140
fun parse_id pos = Option.map Markup.parse_int (get_id pos);
wenzelm@50911
   141
wenzelm@29307
   142
wenzelm@29307
   143
(* markup properties *)
wenzelm@29307
   144
wenzelm@58978
   145
fun get props name =
wenzelm@58978
   146
  (case Properties.get props name of
wenzelm@58978
   147
    NONE => 0
wenzelm@58978
   148
  | SOME s => Markup.parse_int s);
wenzelm@58978
   149
wenzelm@25817
   150
fun of_properties props =
wenzelm@58978
   151
  make {line = get props Markup.lineN,
wenzelm@58978
   152
    offset = get props Markup.offsetN,
wenzelm@58978
   153
    end_offset = get props Markup.end_offsetN,
wenzelm@58978
   154
    props = props};
wenzelm@26003
   155
wenzelm@50254
   156
fun value k i = if valid i then [(k, Markup.print_int i)] else [];
wenzelm@41484
   157
wenzelm@43710
   158
fun properties_of (Pos ((i, j, k), props)) =
wenzelm@50201
   159
  value Markup.lineN i @ value Markup.offsetN j @ value Markup.end_offsetN k @ props;
wenzelm@26003
   160
wenzelm@54038
   161
val def_properties_of = properties_of #> map (fn (x, y) => ("def_" ^ x, y));
wenzelm@42327
   162
wenzelm@57899
   163
fun entity_properties_of def serial pos =
wenzelm@57899
   164
  if def then (Markup.defN, Markup.print_int serial) :: properties_of pos
wenzelm@57899
   165
  else (Markup.refN, Markup.print_int serial) :: def_properties_of pos;
wenzelm@45412
   166
wenzelm@26052
   167
fun default_properties default props =
wenzelm@50201
   168
  if exists (member (op =) Markup.position_properties o #1) props then props
wenzelm@26052
   169
  else properties_of default @ props;
wenzelm@26052
   170
wenzelm@39440
   171
val markup = Markup.properties o properties_of;
wenzelm@39440
   172
wenzelm@39440
   173
wenzelm@39440
   174
(* reports *)
wenzelm@38887
   175
wenzelm@41504
   176
fun is_reported pos = is_some (offset_of pos) andalso is_some (get_id pos);
wenzelm@56459
   177
fun is_reported_range pos = is_reported pos andalso is_some (end_offset_of pos);
wenzelm@30669
   178
wenzelm@41504
   179
fun reported_text pos m txt = if is_reported pos then Markup.markup (markup pos m) txt else "";
wenzelm@56333
   180
fun report_text pos markup txt = Output.report [reported_text pos markup txt];
wenzelm@39507
   181
fun report pos markup = report_text pos markup "";
wenzelm@27764
   182
wenzelm@44736
   183
type report = T * Markup.T;
wenzelm@48767
   184
type report_text = report * string;
wenzelm@44736
   185
wenzelm@48767
   186
val reports_text =
wenzelm@48767
   187
  map (fn ((pos, m), txt) => if is_reported pos then Markup.markup (markup pos m) txt else "")
wenzelm@56333
   188
  #> Output.report;
wenzelm@42204
   189
wenzelm@48767
   190
val reports = map (rpair "") #> reports_text;
wenzelm@48767
   191
wenzelm@44735
   192
fun store_reports _ [] _ _ = ()
wenzelm@55922
   193
  | store_reports (r: report_text list Unsynchronized.ref) ps markup x =
wenzelm@42204
   194
      let val ms = markup x
wenzelm@55922
   195
      in Unsynchronized.change r (fold (fn p => fold (fn m => cons ((p, m), "")) ms) ps) end;
wenzelm@42204
   196
wenzelm@55959
   197
fun append_reports (r: report_text list Unsynchronized.ref) reports =
wenzelm@55959
   198
  Unsynchronized.change r (append (map (rpair "") reports));
wenzelm@55959
   199
wenzelm@25817
   200
wenzelm@56532
   201
(* here: user output *)
wenzelm@26003
   202
wenzelm@48992
   203
fun here pos =
wenzelm@26003
   204
  let
wenzelm@26003
   205
    val props = properties_of pos;
wenzelm@55624
   206
    val (s1, s2) =
wenzelm@26003
   207
      (case (line_of pos, file_of pos) of
wenzelm@55624
   208
        (SOME i, NONE) => (" ", "(line " ^ Markup.print_int i ^ ")")
wenzelm@55624
   209
      | (SOME i, SOME name) => (" ", "(line " ^ Markup.print_int i ^ " of " ^ quote name ^ ")")
wenzelm@55624
   210
      | (NONE, SOME name) => (" ", "(file " ^ quote name ^ ")")
wenzelm@62529
   211
      | _ => if is_reported pos then ("", "\<here>") else ("", ""));
wenzelm@26003
   212
  in
wenzelm@26003
   213
    if null props then ""
wenzelm@55624
   214
    else s1 ^ Markup.markup (Markup.properties props Markup.position) s2
wenzelm@26003
   215
  end;
wenzelm@25817
   216
wenzelm@62803
   217
val here_list = implode o map here;
wenzelm@49691
   218
wenzelm@23627
   219
wenzelm@27736
   220
(* range *)
wenzelm@27736
   221
wenzelm@27736
   222
type range = T * T;
wenzelm@27736
   223
wenzelm@27796
   224
val no_range = (none, none);
wenzelm@27796
   225
wenzelm@62800
   226
fun no_range_position (Pos ((i, j, _), props)) = Pos ((i, j, 0), props);
wenzelm@62797
   227
fun range_position (Pos ((i, j, _), props), Pos ((_, j', _), _)) = Pos ((i, j, j'), props);
wenzelm@62800
   228
fun range (pos, pos') = (range_position (pos, pos'), no_range_position pos');
wenzelm@27777
   229
wenzelm@58978
   230
fun range_of_properties props =
wenzelm@58978
   231
  let
wenzelm@58978
   232
    val pos = of_properties props;
wenzelm@58978
   233
    val pos' =
wenzelm@58978
   234
      make {line = get props Markup.end_lineN,
wenzelm@58978
   235
        offset = get props Markup.end_offsetN,
wenzelm@58978
   236
        end_offset = 0,
wenzelm@58978
   237
        props = props};
wenzelm@58978
   238
  in (pos, pos') end;
wenzelm@58978
   239
wenzelm@58978
   240
fun properties_of_range (pos, pos') =
wenzelm@58978
   241
  properties_of pos @ value Markup.end_lineN (the_default 0 (line_of pos'));
wenzelm@58978
   242
wenzelm@27764
   243
wenzelm@27764
   244
(* thread data *)
wenzelm@27764
   245
wenzelm@62889
   246
val thread_data_var = Thread_Data.var () : T Thread_Data.var;
wenzelm@62889
   247
fun thread_data () = the_default none (Thread_Data.get thread_data_var);
wenzelm@62889
   248
fun setmp_thread_data pos = Thread_Data.setmp thread_data_var (SOME pos);
wenzelm@27764
   249
wenzelm@33097
   250
fun default pos =
wenzelm@49528
   251
  if pos = none then (false, thread_data ())
wenzelm@49528
   252
  else (true, pos);
wenzelm@33097
   253
wenzelm@27764
   254
end;