src/Pure/General/position.ML
author wenzelm
Tue, 27 Nov 2018 16:22:12 +0100
changeset 69348 f0aef5e337a2
parent 68858 e1796b8ddbae
child 70498 de75eea6ffc8
permissions -rw-r--r--
more robust (amending 76979adf0b96);
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
6118
caa439435666 fixed titles;
wenzelm
parents: 5010
diff changeset
     1
(*  Title:      Pure/General/position.ML
5010
9101b70b696d moved Thy/position.ML to General/position.ML;
wenzelm
parents:
diff changeset
     2
    Author:     Markus Wenzel, TU Muenchen
9101b70b696d moved Thy/position.ML to General/position.ML;
wenzelm
parents:
diff changeset
     3
29307
3a0b38b7fbb4 added id;
wenzelm
parents: 28122
diff changeset
     4
Source positions: counting Isabelle symbols, starting from 1.
5010
9101b70b696d moved Thy/position.ML to General/position.ML;
wenzelm
parents:
diff changeset
     5
*)
9101b70b696d moved Thy/position.ML to General/position.ML;
wenzelm
parents:
diff changeset
     6
9101b70b696d moved Thy/position.ML to General/position.ML;
wenzelm
parents:
diff changeset
     7
signature POSITION =
9101b70b696d moved Thy/position.ML to General/position.ML;
wenzelm
parents:
diff changeset
     8
sig
41484
51310e1ccd6f more direct treatment of Position.end_offset;
wenzelm
parents: 41483
diff changeset
     9
  eqtype T
62940
a03592aafadf tuned -- avoid recoding properties;
wenzelm
parents: 62929
diff changeset
    10
  val make: Thread_Position.T -> T
a03592aafadf tuned -- avoid recoding properties;
wenzelm
parents: 62929
diff changeset
    11
  val dest: T -> Thread_Position.T
23673
67c748e5ae54 replaced name by file (unquoted);
wenzelm
parents: 23627
diff changeset
    12
  val line_of: T -> int option
27795
f67f4c677d81 count offset as well;
wenzelm
parents: 27791
diff changeset
    13
  val offset_of: T -> int option
41484
51310e1ccd6f more direct treatment of Position.end_offset;
wenzelm
parents: 41483
diff changeset
    14
  val end_offset_of: T -> int option
23673
67c748e5ae54 replaced name by file (unquoted);
wenzelm
parents: 23627
diff changeset
    15
  val file_of: T -> string option
27796
a6da5f68e776 added distance_of (permissive version);
wenzelm
parents: 27795
diff changeset
    16
  val advance: Symbol.symbol -> T -> T
68183
6560324b1e4d adjust position according to offset of command/exec id;
wenzelm
parents: 68177
diff changeset
    17
  val advance_offsets: int -> T -> T
68177
6e40f5d43936 clarified signature;
wenzelm
parents: 68172
diff changeset
    18
  val distance_of: T * T -> int option
5010
9101b70b696d moved Thy/position.ML to General/position.ML;
wenzelm
parents:
diff changeset
    19
  val none: T
27777
7a63d1b50b88 only increment column if valid;
wenzelm
parents: 27764
diff changeset
    20
  val start: T
31435
d24ef3ff34bc export file_name;
wenzelm
parents: 31424
diff changeset
    21
  val file_name: string -> Properties.T
44200
ce0112e26b3b tuned error message;
wenzelm
parents: 43710
diff changeset
    22
  val file_only: string -> T
27777
7a63d1b50b88 only increment column if valid;
wenzelm
parents: 27764
diff changeset
    23
  val file: string -> T
56437
b14bd153a753 clarified position: no offset here;
wenzelm
parents: 56333
diff changeset
    24
  val line_file_only: int -> string -> T
b14bd153a753 clarified position: no offset here;
wenzelm
parents: 56333
diff changeset
    25
  val line_file: int -> string -> T
5010
9101b70b696d moved Thy/position.ML to General/position.ML;
wenzelm
parents:
diff changeset
    26
  val line: int -> T
67280
dfc5a1503916 clarified default position for empty message pos;
wenzelm
parents: 64556
diff changeset
    27
  val get_props: T -> Properties.T
29307
3a0b38b7fbb4 added id;
wenzelm
parents: 28122
diff changeset
    28
  val id: string -> T
32573
62b5b538408d Isar.define_command: identify transaction;
wenzelm
parents: 32195
diff changeset
    29
  val id_only: string -> T
27426
c0ef698c0904 added get_id/put_id;
wenzelm
parents: 26890
diff changeset
    30
  val get_id: T -> string option
c0ef698c0904 added get_id/put_id;
wenzelm
parents: 26890
diff changeset
    31
  val put_id: string -> T -> T
68858
e1796b8ddbae more accurate position for auxiliary files;
wenzelm
parents: 68829
diff changeset
    32
  val copy_id: T -> T -> T
68829
1a4fa494a4a8 tuned signature;
wenzelm
parents: 68183
diff changeset
    33
  val id_properties_of: T -> Properties.T
50911
ee7fe4230642 more explicit treatment of (optional) exception properties, notably for "serial" -- avoid conflict with startPosition = offset;
wenzelm
parents: 50254
diff changeset
    34
  val parse_id: T -> int option
68183
6560324b1e4d adjust position according to offset of command/exec id;
wenzelm
parents: 68177
diff changeset
    35
  val adjust_offsets: (int -> int option) -> T -> T
28017
4919bd124a58 type Properties.T;
wenzelm
parents: 27796
diff changeset
    36
  val of_properties: Properties.T -> T
4919bd124a58 type Properties.T;
wenzelm
parents: 27796
diff changeset
    37
  val properties_of: T -> Properties.T
68172
0f14cf9c632f more concise information;
wenzelm
parents: 67280
diff changeset
    38
  val offset_properties_of: T -> Properties.T
42327
7c7cc7590eb3 Name_Space.entry_markup: keep def position as separate properties;
wenzelm
parents: 42204
diff changeset
    39
  val def_properties_of: T -> Properties.T
45412
7797f5351ec4 entity markup for bound variables;
wenzelm
parents: 44736
diff changeset
    40
  val entity_properties_of: bool -> serial -> T -> Properties.T
28017
4919bd124a58 type Properties.T;
wenzelm
parents: 27796
diff changeset
    41
  val default_properties: T -> Properties.T -> Properties.T
39440
4c2547af5909 simplified/clarified (Context_)Position.markup/reported_text;
wenzelm
parents: 38887
diff changeset
    42
  val markup: T -> Markup.T -> Markup.T
41504
f0f20a5b54df clarified notion Position.is_reported;
wenzelm
parents: 41484
diff changeset
    43
  val is_reported: T -> bool
56459
38d0b2099743 no report for position singularity, notably for aux. file, especially empty one;
wenzelm
parents: 56437
diff changeset
    44
  val is_reported_range: T -> bool
39507
839873937ddd tuned signature of (Context_)Position.report variants;
wenzelm
parents: 39440
diff changeset
    45
  val reported_text: T -> Markup.T -> string -> string
839873937ddd tuned signature of (Context_)Position.report variants;
wenzelm
parents: 39440
diff changeset
    46
  val report_text: T -> Markup.T -> string -> unit
839873937ddd tuned signature of (Context_)Position.report variants;
wenzelm
parents: 39440
diff changeset
    47
  val report: T -> Markup.T -> unit
44736
c2a3f1c84179 bulk reports for improved message throughput;
wenzelm
parents: 44735
diff changeset
    48
  type report = T * Markup.T
48767
7f0c469cc796 reports with body text, not just markup;
wenzelm
parents: 45666
diff changeset
    49
  type report_text = report * string
7f0c469cc796 reports with body text, not just markup;
wenzelm
parents: 45666
diff changeset
    50
  val reports_text: report_text list -> unit
44736
c2a3f1c84179 bulk reports for improved message throughput;
wenzelm
parents: 44735
diff changeset
    51
  val reports: report list -> unit
55922
710bc66f432c more markup for inner syntax class/type names (notably for completion);
wenzelm
parents: 55624
diff changeset
    52
  val store_reports: report_text list Unsynchronized.ref ->
710bc66f432c more markup for inner syntax class/type names (notably for completion);
wenzelm
parents: 55624
diff changeset
    53
    T list -> ('a -> Markup.T list) -> 'a -> unit
55959
c3b458435f4f more decisive commitment to get_free vs. the_const;
wenzelm
parents: 55922
diff changeset
    54
  val append_reports: report_text list Unsynchronized.ref -> report list -> unit
48992
0518bf89c777 renamed Position.str_of to Position.here;
wenzelm
parents: 48767
diff changeset
    55
  val here: T -> string
49691
74ad6ecf2af2 more error positions;
wenzelm
parents: 49528
diff changeset
    56
  val here_list: T list -> string
27764
e0ee3cc240fe advance: single argument (again);
wenzelm
parents: 27759
diff changeset
    57
  type range = T * T
27796
a6da5f68e776 added distance_of (permissive version);
wenzelm
parents: 27795
diff changeset
    58
  val no_range: range
62800
7ac100f86863 tuned signature;
wenzelm
parents: 62798
diff changeset
    59
  val no_range_position: T -> T
62797
e08c44eed27f tuned signature;
wenzelm
parents: 62750
diff changeset
    60
  val range_position: range -> T
e08c44eed27f tuned signature;
wenzelm
parents: 62750
diff changeset
    61
  val range: T * T -> range
58978
e42da880c61e more position information, e.g. relevant for errors in generated ML source;
wenzelm
parents: 58854
diff changeset
    62
  val range_of_properties: Properties.T -> range
e42da880c61e more position information, e.g. relevant for errors in generated ML source;
wenzelm
parents: 58854
diff changeset
    63
  val properties_of_range: range -> Properties.T
25817
d8e0190917a5 type T: based on properties, added id field;
wenzelm
parents: 25792
diff changeset
    64
  val thread_data: unit -> T
d8e0190917a5 type T: based on properties, added id field;
wenzelm
parents: 25792
diff changeset
    65
  val setmp_thread_data: T -> ('a -> 'b) -> 'a -> 'b
49528
789b73fcca72 report proper binding positions only -- avoid swamping document model with unspecific information;
wenzelm
parents: 48992
diff changeset
    66
  val default: T -> bool * T
5010
9101b70b696d moved Thy/position.ML to General/position.ML;
wenzelm
parents:
diff changeset
    67
end;
9101b70b696d moved Thy/position.ML to General/position.ML;
wenzelm
parents:
diff changeset
    68
9101b70b696d moved Thy/position.ML to General/position.ML;
wenzelm
parents:
diff changeset
    69
structure Position: POSITION =
9101b70b696d moved Thy/position.ML to General/position.ML;
wenzelm
parents:
diff changeset
    70
struct
9101b70b696d moved Thy/position.ML to General/position.ML;
wenzelm
parents:
diff changeset
    71
9101b70b696d moved Thy/position.ML to General/position.ML;
wenzelm
parents:
diff changeset
    72
(* datatype position *)
9101b70b696d moved Thy/position.ML to General/position.ML;
wenzelm
parents:
diff changeset
    73
43710
7270ae921cf2 discontinued odd Position.column -- left-over from attempts at PGIP implementation;
wenzelm
parents: 42818
diff changeset
    74
datatype T = Pos of (int * int * int) * Properties.T;
41484
51310e1ccd6f more direct treatment of Position.end_offset;
wenzelm
parents: 41483
diff changeset
    75
51310e1ccd6f more direct treatment of Position.end_offset;
wenzelm
parents: 41483
diff changeset
    76
fun norm_props (props: Properties.T) =
45666
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45412
diff changeset
    77
  maps (fn a => the_list (find_first (fn (b, _) => a = b) props))
50201
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49691
diff changeset
    78
    Markup.position_properties';
41484
51310e1ccd6f more direct treatment of Position.end_offset;
wenzelm
parents: 41483
diff changeset
    79
43710
7270ae921cf2 discontinued odd Position.column -- left-over from attempts at PGIP implementation;
wenzelm
parents: 42818
diff changeset
    80
fun make {line = i, offset = j, end_offset = k, props} = Pos ((i, j, k), norm_props props);
7270ae921cf2 discontinued odd Position.column -- left-over from attempts at PGIP implementation;
wenzelm
parents: 42818
diff changeset
    81
fun dest (Pos ((i, j, k), props)) = {line = i, offset = j, end_offset = k, props = props};
27777
7a63d1b50b88 only increment column if valid;
wenzelm
parents: 27764
diff changeset
    82
27795
f67f4c677d81 count offset as well;
wenzelm
parents: 27791
diff changeset
    83
fun valid (i: int) = i > 0;
f67f4c677d81 count offset as well;
wenzelm
parents: 27791
diff changeset
    84
fun if_valid i i' = if valid i then i' else i;
f67f4c677d81 count offset as well;
wenzelm
parents: 27791
diff changeset
    85
27777
7a63d1b50b88 only increment column if valid;
wenzelm
parents: 27764
diff changeset
    86
27796
a6da5f68e776 added distance_of (permissive version);
wenzelm
parents: 27795
diff changeset
    87
(* fields *)
a6da5f68e776 added distance_of (permissive version);
wenzelm
parents: 27795
diff changeset
    88
43710
7270ae921cf2 discontinued odd Position.column -- left-over from attempts at PGIP implementation;
wenzelm
parents: 42818
diff changeset
    89
fun line_of (Pos ((i, _, _), _)) = if valid i then SOME i else NONE;
7270ae921cf2 discontinued odd Position.column -- left-over from attempts at PGIP implementation;
wenzelm
parents: 42818
diff changeset
    90
fun offset_of (Pos ((_, j, _), _)) = if valid j then SOME j else NONE;
7270ae921cf2 discontinued odd Position.column -- left-over from attempts at PGIP implementation;
wenzelm
parents: 42818
diff changeset
    91
fun end_offset_of (Pos ((_, _, k), _)) = if valid k then SOME k else NONE;
27796
a6da5f68e776 added distance_of (permissive version);
wenzelm
parents: 27795
diff changeset
    92
50201
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49691
diff changeset
    93
fun file_of (Pos (_, props)) = Properties.get props Markup.fileN;
27796
a6da5f68e776 added distance_of (permissive version);
wenzelm
parents: 27795
diff changeset
    94
a6da5f68e776 added distance_of (permissive version);
wenzelm
parents: 27795
diff changeset
    95
27777
7a63d1b50b88 only increment column if valid;
wenzelm
parents: 27764
diff changeset
    96
(* advance *)
26003
7a8aee8353cf added column field;
wenzelm
parents: 25954
diff changeset
    97
43710
7270ae921cf2 discontinued odd Position.column -- left-over from attempts at PGIP implementation;
wenzelm
parents: 42818
diff changeset
    98
fun advance_count "\n" (i: int, j: int, k: int) =
7270ae921cf2 discontinued odd Position.column -- left-over from attempts at PGIP implementation;
wenzelm
parents: 42818
diff changeset
    99
      (if_valid i (i + 1), if_valid j (j + 1), k)
7270ae921cf2 discontinued odd Position.column -- left-over from attempts at PGIP implementation;
wenzelm
parents: 42818
diff changeset
   100
  | advance_count s (i, j, k) =
58854
b979c781c2db discontinued obsolete \<^sync> marker;
wenzelm
parents: 57899
diff changeset
   101
      if Symbol.not_eof s then (i, if_valid j (j + 1), k)
43710
7270ae921cf2 discontinued odd Position.column -- left-over from attempts at PGIP implementation;
wenzelm
parents: 42818
diff changeset
   102
      else (i, j, k);
5010
9101b70b696d moved Thy/position.ML to General/position.ML;
wenzelm
parents:
diff changeset
   103
43710
7270ae921cf2 discontinued odd Position.column -- left-over from attempts at PGIP implementation;
wenzelm
parents: 42818
diff changeset
   104
fun invalid_count (i, j, _: int) =
7270ae921cf2 discontinued odd Position.column -- left-over from attempts at PGIP implementation;
wenzelm
parents: 42818
diff changeset
   105
  not (valid i orelse valid j);
27795
f67f4c677d81 count offset as well;
wenzelm
parents: 27791
diff changeset
   106
f67f4c677d81 count offset as well;
wenzelm
parents: 27791
diff changeset
   107
fun advance sym (pos as (Pos (count, props))) =
f67f4c677d81 count offset as well;
wenzelm
parents: 27791
diff changeset
   108
  if invalid_count count then pos else Pos (advance_count sym count, props);
27777
7a63d1b50b88 only increment column if valid;
wenzelm
parents: 27764
diff changeset
   109
68183
6560324b1e4d adjust position according to offset of command/exec id;
wenzelm
parents: 68177
diff changeset
   110
fun advance_offsets offset (pos as (Pos (count as (i, j, k), props))) =
6560324b1e4d adjust position according to offset of command/exec id;
wenzelm
parents: 68177
diff changeset
   111
  if offset = 0 orelse invalid_count count then pos
6560324b1e4d adjust position according to offset of command/exec id;
wenzelm
parents: 68177
diff changeset
   112
  else if offset < 0 then raise Fail "Illegal offset"
59085
08a6901eb035 clarified define_command: send tokens more directly, without requiring keywords in ML;
wenzelm
parents: 58978
diff changeset
   113
  else if valid i then raise Fail "Illegal line position"
68183
6560324b1e4d adjust position according to offset of command/exec id;
wenzelm
parents: 68177
diff changeset
   114
  else Pos ((i, if_valid j (j + offset), if_valid k (k + offset)), props);
59085
08a6901eb035 clarified define_command: send tokens more directly, without requiring keywords in ML;
wenzelm
parents: 58978
diff changeset
   115
27777
7a63d1b50b88 only increment column if valid;
wenzelm
parents: 27764
diff changeset
   116
27796
a6da5f68e776 added distance_of (permissive version);
wenzelm
parents: 27795
diff changeset
   117
(* distance of adjacent positions *)
27777
7a63d1b50b88 only increment column if valid;
wenzelm
parents: 27764
diff changeset
   118
68177
6e40f5d43936 clarified signature;
wenzelm
parents: 68172
diff changeset
   119
fun distance_of (Pos ((_, j, _), _), Pos ((_, j', _), _)) =
6e40f5d43936 clarified signature;
wenzelm
parents: 68172
diff changeset
   120
  if valid j andalso valid j' then SOME (j' - j) else NONE;
26882
9e824d8f4512 renamed Position.path to Path.position;
wenzelm
parents: 26633
diff changeset
   121
5010
9101b70b696d moved Thy/position.ML to General/position.ML;
wenzelm
parents:
diff changeset
   122
27777
7a63d1b50b88 only increment column if valid;
wenzelm
parents: 27764
diff changeset
   123
(* make position *)
7a63d1b50b88 only increment column if valid;
wenzelm
parents: 27764
diff changeset
   124
43710
7270ae921cf2 discontinued odd Position.column -- left-over from attempts at PGIP implementation;
wenzelm
parents: 42818
diff changeset
   125
val none = Pos ((0, 0, 0), []);
7270ae921cf2 discontinued odd Position.column -- left-over from attempts at PGIP implementation;
wenzelm
parents: 42818
diff changeset
   126
val start = Pos ((1, 1, 0), []);
27744
d4c5ddf98869 advance: operate on symbol list (less overhead);
wenzelm
parents: 27741
diff changeset
   127
29307
3a0b38b7fbb4 added id;
wenzelm
parents: 28122
diff changeset
   128
27796
a6da5f68e776 added distance_of (permissive version);
wenzelm
parents: 27795
diff changeset
   129
fun file_name "" = []
50201
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49691
diff changeset
   130
  | file_name name = [(Markup.fileN, name)];
27796
a6da5f68e776 added distance_of (permissive version);
wenzelm
parents: 27795
diff changeset
   131
44200
ce0112e26b3b tuned error message;
wenzelm
parents: 43710
diff changeset
   132
fun file_only name = Pos ((0, 0, 0), file_name name);
43710
7270ae921cf2 discontinued odd Position.column -- left-over from attempts at PGIP implementation;
wenzelm
parents: 42818
diff changeset
   133
fun file name = Pos ((1, 1, 0), file_name name);
27744
d4c5ddf98869 advance: operate on symbol list (less overhead);
wenzelm
parents: 27741
diff changeset
   134
56437
b14bd153a753 clarified position: no offset here;
wenzelm
parents: 56333
diff changeset
   135
fun line_file_only i name = Pos ((i, 0, 0), file_name name);
43710
7270ae921cf2 discontinued odd Position.column -- left-over from attempts at PGIP implementation;
wenzelm
parents: 42818
diff changeset
   136
fun line_file i name = Pos ((i, 1, 0), file_name name);
27795
f67f4c677d81 count offset as well;
wenzelm
parents: 27791
diff changeset
   137
fun line i = line_file i "";
5010
9101b70b696d moved Thy/position.ML to General/position.ML;
wenzelm
parents:
diff changeset
   138
67280
dfc5a1503916 clarified default position for empty message pos;
wenzelm
parents: 64556
diff changeset
   139
fun get_props (Pos (_, props)) = props;
dfc5a1503916 clarified default position for empty message pos;
wenzelm
parents: 64556
diff changeset
   140
50201
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49691
diff changeset
   141
fun id id = Pos ((0, 1, 0), [(Markup.idN, id)]);
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49691
diff changeset
   142
fun id_only id = Pos ((0, 0, 0), [(Markup.idN, id)]);
22158
ff4fc4ee9eb0 Add line_of, name_of destructors.
aspinall
parents: 15531
diff changeset
   143
50201
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49691
diff changeset
   144
fun get_id (Pos (_, props)) = Properties.get props Markup.idN;
62750
3f8f7aa1b11e proper norm_props, e.g. relevant for ML pp;
wenzelm
parents: 62529
diff changeset
   145
fun put_id id (Pos (count, props)) = Pos (count, norm_props (Properties.put (Markup.idN, id) props));
68858
e1796b8ddbae more accurate position for auxiliary files;
wenzelm
parents: 68829
diff changeset
   146
fun copy_id pos = (case get_id pos of NONE => I | SOME id => put_id id);
27426
c0ef698c0904 added get_id/put_id;
wenzelm
parents: 26890
diff changeset
   147
63806
c54a53ef1873 clarified modules;
wenzelm
parents: 62940
diff changeset
   148
fun parse_id pos = Option.map Value.parse_int (get_id pos);
50911
ee7fe4230642 more explicit treatment of (optional) exception properties, notably for "serial" -- avoid conflict with startPosition = offset;
wenzelm
parents: 50254
diff changeset
   149
68829
1a4fa494a4a8 tuned signature;
wenzelm
parents: 68183
diff changeset
   150
fun id_properties_of pos =
1a4fa494a4a8 tuned signature;
wenzelm
parents: 68183
diff changeset
   151
  (case get_id pos of
1a4fa494a4a8 tuned signature;
wenzelm
parents: 68183
diff changeset
   152
    SOME id => [(Markup.idN, id)]
1a4fa494a4a8 tuned signature;
wenzelm
parents: 68183
diff changeset
   153
  | NONE => []);
29307
3a0b38b7fbb4 added id;
wenzelm
parents: 28122
diff changeset
   154
68183
6560324b1e4d adjust position according to offset of command/exec id;
wenzelm
parents: 68177
diff changeset
   155
fun adjust_offsets adjust (pos as Pos (_, props)) =
68858
e1796b8ddbae more accurate position for auxiliary files;
wenzelm
parents: 68829
diff changeset
   156
  if is_none (file_of pos) then
e1796b8ddbae more accurate position for auxiliary files;
wenzelm
parents: 68829
diff changeset
   157
    (case parse_id pos of
e1796b8ddbae more accurate position for auxiliary files;
wenzelm
parents: 68829
diff changeset
   158
      SOME id =>
e1796b8ddbae more accurate position for auxiliary files;
wenzelm
parents: 68829
diff changeset
   159
        (case adjust id of
e1796b8ddbae more accurate position for auxiliary files;
wenzelm
parents: 68829
diff changeset
   160
          SOME offset =>
e1796b8ddbae more accurate position for auxiliary files;
wenzelm
parents: 68829
diff changeset
   161
            let val Pos (count, _) = advance_offsets offset pos
e1796b8ddbae more accurate position for auxiliary files;
wenzelm
parents: 68829
diff changeset
   162
            in Pos (count, Properties.remove Markup.idN props) end
e1796b8ddbae more accurate position for auxiliary files;
wenzelm
parents: 68829
diff changeset
   163
        | NONE => pos)
e1796b8ddbae more accurate position for auxiliary files;
wenzelm
parents: 68829
diff changeset
   164
    | NONE => pos)
e1796b8ddbae more accurate position for auxiliary files;
wenzelm
parents: 68829
diff changeset
   165
  else pos;
68183
6560324b1e4d adjust position according to offset of command/exec id;
wenzelm
parents: 68177
diff changeset
   166
6560324b1e4d adjust position according to offset of command/exec id;
wenzelm
parents: 68177
diff changeset
   167
29307
3a0b38b7fbb4 added id;
wenzelm
parents: 28122
diff changeset
   168
(* markup properties *)
3a0b38b7fbb4 added id;
wenzelm
parents: 28122
diff changeset
   169
58978
e42da880c61e more position information, e.g. relevant for errors in generated ML source;
wenzelm
parents: 58854
diff changeset
   170
fun get props name =
e42da880c61e more position information, e.g. relevant for errors in generated ML source;
wenzelm
parents: 58854
diff changeset
   171
  (case Properties.get props name of
e42da880c61e more position information, e.g. relevant for errors in generated ML source;
wenzelm
parents: 58854
diff changeset
   172
    NONE => 0
63806
c54a53ef1873 clarified modules;
wenzelm
parents: 62940
diff changeset
   173
  | SOME s => Value.parse_int s);
58978
e42da880c61e more position information, e.g. relevant for errors in generated ML source;
wenzelm
parents: 58854
diff changeset
   174
25817
d8e0190917a5 type T: based on properties, added id field;
wenzelm
parents: 25792
diff changeset
   175
fun of_properties props =
58978
e42da880c61e more position information, e.g. relevant for errors in generated ML source;
wenzelm
parents: 58854
diff changeset
   176
  make {line = get props Markup.lineN,
e42da880c61e more position information, e.g. relevant for errors in generated ML source;
wenzelm
parents: 58854
diff changeset
   177
    offset = get props Markup.offsetN,
e42da880c61e more position information, e.g. relevant for errors in generated ML source;
wenzelm
parents: 58854
diff changeset
   178
    end_offset = get props Markup.end_offsetN,
e42da880c61e more position information, e.g. relevant for errors in generated ML source;
wenzelm
parents: 58854
diff changeset
   179
    props = props};
26003
7a8aee8353cf added column field;
wenzelm
parents: 25954
diff changeset
   180
63806
c54a53ef1873 clarified modules;
wenzelm
parents: 62940
diff changeset
   181
fun value k i = if valid i then [(k, Value.print_int i)] else [];
41484
51310e1ccd6f more direct treatment of Position.end_offset;
wenzelm
parents: 41483
diff changeset
   182
43710
7270ae921cf2 discontinued odd Position.column -- left-over from attempts at PGIP implementation;
wenzelm
parents: 42818
diff changeset
   183
fun properties_of (Pos ((i, j, k), props)) =
50201
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49691
diff changeset
   184
  value Markup.lineN i @ value Markup.offsetN j @ value Markup.end_offsetN k @ props;
26003
7a8aee8353cf added column field;
wenzelm
parents: 25954
diff changeset
   185
68172
0f14cf9c632f more concise information;
wenzelm
parents: 67280
diff changeset
   186
fun offset_properties_of (Pos ((_, j, k), _)) =
0f14cf9c632f more concise information;
wenzelm
parents: 67280
diff changeset
   187
  value Markup.offsetN j @ value Markup.end_offsetN k;
0f14cf9c632f more concise information;
wenzelm
parents: 67280
diff changeset
   188
54038
wenzelm
parents: 50911
diff changeset
   189
val def_properties_of = properties_of #> map (fn (x, y) => ("def_" ^ x, y));
42327
7c7cc7590eb3 Name_Space.entry_markup: keep def position as separate properties;
wenzelm
parents: 42204
diff changeset
   190
57899
5867d1306712 clarified signature: entity serial number is not position id;
wenzelm
parents: 56532
diff changeset
   191
fun entity_properties_of def serial pos =
63806
c54a53ef1873 clarified modules;
wenzelm
parents: 62940
diff changeset
   192
  if def then (Markup.defN, Value.print_int serial) :: properties_of pos
c54a53ef1873 clarified modules;
wenzelm
parents: 62940
diff changeset
   193
  else (Markup.refN, Value.print_int serial) :: def_properties_of pos;
45412
7797f5351ec4 entity markup for bound variables;
wenzelm
parents: 44736
diff changeset
   194
26052
7d5b3e34a735 added default_properties;
wenzelm
parents: 26003
diff changeset
   195
fun default_properties default props =
50201
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49691
diff changeset
   196
  if exists (member (op =) Markup.position_properties o #1) props then props
26052
7d5b3e34a735 added default_properties;
wenzelm
parents: 26003
diff changeset
   197
  else properties_of default @ props;
7d5b3e34a735 added default_properties;
wenzelm
parents: 26003
diff changeset
   198
39440
4c2547af5909 simplified/clarified (Context_)Position.markup/reported_text;
wenzelm
parents: 38887
diff changeset
   199
val markup = Markup.properties o properties_of;
4c2547af5909 simplified/clarified (Context_)Position.markup/reported_text;
wenzelm
parents: 38887
diff changeset
   200
4c2547af5909 simplified/clarified (Context_)Position.markup/reported_text;
wenzelm
parents: 38887
diff changeset
   201
4c2547af5909 simplified/clarified (Context_)Position.markup/reported_text;
wenzelm
parents: 38887
diff changeset
   202
(* reports *)
38887
1261481ef5e5 Command.State: add reported positions to markup tree, according main message position or Markup.binding/entity/report occurrences in body;
wenzelm
parents: 38236
diff changeset
   203
41504
f0f20a5b54df clarified notion Position.is_reported;
wenzelm
parents: 41484
diff changeset
   204
fun is_reported pos = is_some (offset_of pos) andalso is_some (get_id pos);
56459
38d0b2099743 no report for position singularity, notably for aux. file, especially empty one;
wenzelm
parents: 56437
diff changeset
   205
fun is_reported_range pos = is_reported pos andalso is_some (end_offset_of pos);
30669
6de7ef888aa3 added report_text -- status messages with text body;
wenzelm
parents: 29307
diff changeset
   206
41504
f0f20a5b54df clarified notion Position.is_reported;
wenzelm
parents: 41484
diff changeset
   207
fun reported_text pos m txt = if is_reported pos then Markup.markup (markup pos m) txt else "";
56333
38f1422ef473 support bulk messages consisting of small string segments, which are more healthy to the Poly/ML RTS and might prevent spurious GC crashes such as MTGCProcessMarkPointers::ScanAddressesInObject;
wenzelm
parents: 55959
diff changeset
   208
fun report_text pos markup txt = Output.report [reported_text pos markup txt];
39507
839873937ddd tuned signature of (Context_)Position.report variants;
wenzelm
parents: 39440
diff changeset
   209
fun report pos markup = report_text pos markup "";
27764
e0ee3cc240fe advance: single argument (again);
wenzelm
parents: 27759
diff changeset
   210
44736
c2a3f1c84179 bulk reports for improved message throughput;
wenzelm
parents: 44735
diff changeset
   211
type report = T * Markup.T;
48767
7f0c469cc796 reports with body text, not just markup;
wenzelm
parents: 45666
diff changeset
   212
type report_text = report * string;
44736
c2a3f1c84179 bulk reports for improved message throughput;
wenzelm
parents: 44735
diff changeset
   213
48767
7f0c469cc796 reports with body text, not just markup;
wenzelm
parents: 45666
diff changeset
   214
val reports_text =
7f0c469cc796 reports with body text, not just markup;
wenzelm
parents: 45666
diff changeset
   215
  map (fn ((pos, m), txt) => if is_reported pos then Markup.markup (markup pos m) txt else "")
56333
38f1422ef473 support bulk messages consisting of small string segments, which are more healthy to the Poly/ML RTS and might prevent spurious GC crashes such as MTGCProcessMarkPointers::ScanAddressesInObject;
wenzelm
parents: 55959
diff changeset
   216
  #> Output.report;
42204
b3277168c1e7 added Position.reports convenience;
wenzelm
parents: 41504
diff changeset
   217
48767
7f0c469cc796 reports with body text, not just markup;
wenzelm
parents: 45666
diff changeset
   218
val reports = map (rpair "") #> reports_text;
7f0c469cc796 reports with body text, not just markup;
wenzelm
parents: 45666
diff changeset
   219
44735
66862d02678c tuned signature;
wenzelm
parents: 44224
diff changeset
   220
fun store_reports _ [] _ _ = ()
55922
710bc66f432c more markup for inner syntax class/type names (notably for completion);
wenzelm
parents: 55624
diff changeset
   221
  | store_reports (r: report_text list Unsynchronized.ref) ps markup x =
42204
b3277168c1e7 added Position.reports convenience;
wenzelm
parents: 41504
diff changeset
   222
      let val ms = markup x
55922
710bc66f432c more markup for inner syntax class/type names (notably for completion);
wenzelm
parents: 55624
diff changeset
   223
      in Unsynchronized.change r (fold (fn p => fold (fn m => cons ((p, m), "")) ms) ps) end;
42204
b3277168c1e7 added Position.reports convenience;
wenzelm
parents: 41504
diff changeset
   224
55959
c3b458435f4f more decisive commitment to get_free vs. the_const;
wenzelm
parents: 55922
diff changeset
   225
fun append_reports (r: report_text list Unsynchronized.ref) reports =
c3b458435f4f more decisive commitment to get_free vs. the_const;
wenzelm
parents: 55922
diff changeset
   226
  Unsynchronized.change r (append (map (rpair "") reports));
c3b458435f4f more decisive commitment to get_free vs. the_const;
wenzelm
parents: 55922
diff changeset
   227
25817
d8e0190917a5 type T: based on properties, added id field;
wenzelm
parents: 25792
diff changeset
   228
56532
3da244bc02bd tuned message, to accommodate extra brackets produced by Scala parsers;
wenzelm
parents: 56459
diff changeset
   229
(* here: user output *)
26003
7a8aee8353cf added column field;
wenzelm
parents: 25954
diff changeset
   230
48992
0518bf89c777 renamed Position.str_of to Position.here;
wenzelm
parents: 48767
diff changeset
   231
fun here pos =
26003
7a8aee8353cf added column field;
wenzelm
parents: 25954
diff changeset
   232
  let
7a8aee8353cf added column field;
wenzelm
parents: 25954
diff changeset
   233
    val props = properties_of pos;
55624
d52409077135 tuned messages;
wenzelm
parents: 55546
diff changeset
   234
    val (s1, s2) =
26003
7a8aee8353cf added column field;
wenzelm
parents: 25954
diff changeset
   235
      (case (line_of pos, file_of pos) of
63806
c54a53ef1873 clarified modules;
wenzelm
parents: 62940
diff changeset
   236
        (SOME i, NONE) => (" ", "(line " ^ Value.print_int i ^ ")")
c54a53ef1873 clarified modules;
wenzelm
parents: 62940
diff changeset
   237
      | (SOME i, SOME name) => (" ", "(line " ^ Value.print_int i ^ " of " ^ quote name ^ ")")
55624
d52409077135 tuned messages;
wenzelm
parents: 55546
diff changeset
   238
      | (NONE, SOME name) => (" ", "(file " ^ quote name ^ ")")
64556
851ae0e7b09c more symbols;
wenzelm
parents: 63806
diff changeset
   239
      | _ => if is_reported pos then ("", "\092<^here>") else ("", ""));
26003
7a8aee8353cf added column field;
wenzelm
parents: 25954
diff changeset
   240
  in
69348
f0aef5e337a2 more robust (amending 76979adf0b96);
wenzelm
parents: 68858
diff changeset
   241
    if s2 = "" then ""
55624
d52409077135 tuned messages;
wenzelm
parents: 55546
diff changeset
   242
    else s1 ^ Markup.markup (Markup.properties props Markup.position) s2
26003
7a8aee8353cf added column field;
wenzelm
parents: 25954
diff changeset
   243
  end;
25817
d8e0190917a5 type T: based on properties, added id field;
wenzelm
parents: 25792
diff changeset
   244
62803
5f73bf6ba98b required space is already part of Position.here;
wenzelm
parents: 62800
diff changeset
   245
val here_list = implode o map here;
49691
74ad6ecf2af2 more error positions;
wenzelm
parents: 49528
diff changeset
   246
23627
f543538866a2 added property conversions;
wenzelm
parents: 22158
diff changeset
   247
27736
3703dbd0cdea added encode_range;
wenzelm
parents: 27661
diff changeset
   248
(* range *)
3703dbd0cdea added encode_range;
wenzelm
parents: 27661
diff changeset
   249
3703dbd0cdea added encode_range;
wenzelm
parents: 27661
diff changeset
   250
type range = T * T;
3703dbd0cdea added encode_range;
wenzelm
parents: 27661
diff changeset
   251
27796
a6da5f68e776 added distance_of (permissive version);
wenzelm
parents: 27795
diff changeset
   252
val no_range = (none, none);
a6da5f68e776 added distance_of (permissive version);
wenzelm
parents: 27795
diff changeset
   253
62800
7ac100f86863 tuned signature;
wenzelm
parents: 62798
diff changeset
   254
fun no_range_position (Pos ((i, j, _), props)) = Pos ((i, j, 0), props);
62797
e08c44eed27f tuned signature;
wenzelm
parents: 62750
diff changeset
   255
fun range_position (Pos ((i, j, _), props), Pos ((_, j', _), _)) = Pos ((i, j, j'), props);
62800
7ac100f86863 tuned signature;
wenzelm
parents: 62798
diff changeset
   256
fun range (pos, pos') = (range_position (pos, pos'), no_range_position pos');
27777
7a63d1b50b88 only increment column if valid;
wenzelm
parents: 27764
diff changeset
   257
58978
e42da880c61e more position information, e.g. relevant for errors in generated ML source;
wenzelm
parents: 58854
diff changeset
   258
fun range_of_properties props =
e42da880c61e more position information, e.g. relevant for errors in generated ML source;
wenzelm
parents: 58854
diff changeset
   259
  let
e42da880c61e more position information, e.g. relevant for errors in generated ML source;
wenzelm
parents: 58854
diff changeset
   260
    val pos = of_properties props;
e42da880c61e more position information, e.g. relevant for errors in generated ML source;
wenzelm
parents: 58854
diff changeset
   261
    val pos' =
e42da880c61e more position information, e.g. relevant for errors in generated ML source;
wenzelm
parents: 58854
diff changeset
   262
      make {line = get props Markup.end_lineN,
e42da880c61e more position information, e.g. relevant for errors in generated ML source;
wenzelm
parents: 58854
diff changeset
   263
        offset = get props Markup.end_offsetN,
e42da880c61e more position information, e.g. relevant for errors in generated ML source;
wenzelm
parents: 58854
diff changeset
   264
        end_offset = 0,
e42da880c61e more position information, e.g. relevant for errors in generated ML source;
wenzelm
parents: 58854
diff changeset
   265
        props = props};
e42da880c61e more position information, e.g. relevant for errors in generated ML source;
wenzelm
parents: 58854
diff changeset
   266
  in (pos, pos') end;
e42da880c61e more position information, e.g. relevant for errors in generated ML source;
wenzelm
parents: 58854
diff changeset
   267
e42da880c61e more position information, e.g. relevant for errors in generated ML source;
wenzelm
parents: 58854
diff changeset
   268
fun properties_of_range (pos, pos') =
e42da880c61e more position information, e.g. relevant for errors in generated ML source;
wenzelm
parents: 58854
diff changeset
   269
  properties_of pos @ value Markup.end_lineN (the_default 0 (line_of pos'));
e42da880c61e more position information, e.g. relevant for errors in generated ML source;
wenzelm
parents: 58854
diff changeset
   270
27764
e0ee3cc240fe advance: single argument (again);
wenzelm
parents: 27759
diff changeset
   271
e0ee3cc240fe advance: single argument (again);
wenzelm
parents: 27759
diff changeset
   272
(* thread data *)
e0ee3cc240fe advance: single argument (again);
wenzelm
parents: 27759
diff changeset
   273
62940
a03592aafadf tuned -- avoid recoding properties;
wenzelm
parents: 62929
diff changeset
   274
val thread_data = make o Thread_Position.get;
a03592aafadf tuned -- avoid recoding properties;
wenzelm
parents: 62929
diff changeset
   275
fun setmp_thread_data pos = Thread_Position.setmp (dest pos);
27764
e0ee3cc240fe advance: single argument (again);
wenzelm
parents: 27759
diff changeset
   276
33097
9d501e11084a maintain position of formal entities via name space;
wenzelm
parents: 32573
diff changeset
   277
fun default pos =
49528
789b73fcca72 report proper binding positions only -- avoid swamping document model with unspecific information;
wenzelm
parents: 48992
diff changeset
   278
  if pos = none then (false, thread_data ())
789b73fcca72 report proper binding positions only -- avoid swamping document model with unspecific information;
wenzelm
parents: 48992
diff changeset
   279
  else (true, pos);
33097
9d501e11084a maintain position of formal entities via name space;
wenzelm
parents: 32573
diff changeset
   280
27764
e0ee3cc240fe advance: single argument (again);
wenzelm
parents: 27759
diff changeset
   281
end;