src/Pure/General/position.ML
author wenzelm
Sun, 10 Apr 2016 17:52:30 +0200
changeset 62940 a03592aafadf
parent 62929 b92565f98206
child 63806 c54a53ef1873
permissions -rw-r--r--
tuned -- avoid recoding properties;
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
59085
08a6901eb035 clarified define_command: send tokens more directly, without requiring keywords in ML;
wenzelm
parents: 58978
diff changeset
    17
  val advance_offset: int -> T -> T
27796
a6da5f68e776 added distance_of (permissive version);
wenzelm
parents: 27795
diff changeset
    18
  val distance_of: T -> T -> int
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
29307
3a0b38b7fbb4 added id;
wenzelm
parents: 28122
diff changeset
    27
  val id: string -> T
32573
62b5b538408d Isar.define_command: identify transaction;
wenzelm
parents: 32195
diff changeset
    28
  val id_only: string -> T
27426
c0ef698c0904 added get_id/put_id;
wenzelm
parents: 26890
diff changeset
    29
  val get_id: T -> string option
c0ef698c0904 added get_id/put_id;
wenzelm
parents: 26890
diff changeset
    30
  val put_id: string -> T -> T
50911
ee7fe4230642 more explicit treatment of (optional) exception properties, notably for "serial" -- avoid conflict with startPosition = offset;
wenzelm
parents: 50254
diff changeset
    31
  val parse_id: T -> int option
28017
4919bd124a58 type Properties.T;
wenzelm
parents: 27796
diff changeset
    32
  val of_properties: Properties.T -> T
4919bd124a58 type Properties.T;
wenzelm
parents: 27796
diff changeset
    33
  val properties_of: T -> Properties.T
42327
7c7cc7590eb3 Name_Space.entry_markup: keep def position as separate properties;
wenzelm
parents: 42204
diff changeset
    34
  val def_properties_of: T -> Properties.T
45412
7797f5351ec4 entity markup for bound variables;
wenzelm
parents: 44736
diff changeset
    35
  val entity_properties_of: bool -> serial -> T -> Properties.T
28017
4919bd124a58 type Properties.T;
wenzelm
parents: 27796
diff changeset
    36
  val default_properties: T -> Properties.T -> Properties.T
39440
4c2547af5909 simplified/clarified (Context_)Position.markup/reported_text;
wenzelm
parents: 38887
diff changeset
    37
  val markup: T -> Markup.T -> Markup.T
41504
f0f20a5b54df clarified notion Position.is_reported;
wenzelm
parents: 41484
diff changeset
    38
  val is_reported: T -> bool
56459
38d0b2099743 no report for position singularity, notably for aux. file, especially empty one;
wenzelm
parents: 56437
diff changeset
    39
  val is_reported_range: T -> bool
39507
839873937ddd tuned signature of (Context_)Position.report variants;
wenzelm
parents: 39440
diff changeset
    40
  val reported_text: T -> Markup.T -> string -> string
839873937ddd tuned signature of (Context_)Position.report variants;
wenzelm
parents: 39440
diff changeset
    41
  val report_text: T -> Markup.T -> string -> unit
839873937ddd tuned signature of (Context_)Position.report variants;
wenzelm
parents: 39440
diff changeset
    42
  val report: T -> Markup.T -> unit
44736
c2a3f1c84179 bulk reports for improved message throughput;
wenzelm
parents: 44735
diff changeset
    43
  type report = T * Markup.T
48767
7f0c469cc796 reports with body text, not just markup;
wenzelm
parents: 45666
diff changeset
    44
  type report_text = report * string
7f0c469cc796 reports with body text, not just markup;
wenzelm
parents: 45666
diff changeset
    45
  val reports_text: report_text list -> unit
44736
c2a3f1c84179 bulk reports for improved message throughput;
wenzelm
parents: 44735
diff changeset
    46
  val reports: report list -> unit
55922
710bc66f432c more markup for inner syntax class/type names (notably for completion);
wenzelm
parents: 55624
diff changeset
    47
  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
    48
    T list -> ('a -> Markup.T list) -> 'a -> unit
55959
c3b458435f4f more decisive commitment to get_free vs. the_const;
wenzelm
parents: 55922
diff changeset
    49
  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
    50
  val here: T -> string
49691
74ad6ecf2af2 more error positions;
wenzelm
parents: 49528
diff changeset
    51
  val here_list: T list -> string
27764
e0ee3cc240fe advance: single argument (again);
wenzelm
parents: 27759
diff changeset
    52
  type range = T * T
27796
a6da5f68e776 added distance_of (permissive version);
wenzelm
parents: 27795
diff changeset
    53
  val no_range: range
62800
7ac100f86863 tuned signature;
wenzelm
parents: 62798
diff changeset
    54
  val no_range_position: T -> T
62797
e08c44eed27f tuned signature;
wenzelm
parents: 62750
diff changeset
    55
  val range_position: range -> T
e08c44eed27f tuned signature;
wenzelm
parents: 62750
diff changeset
    56
  val range: T * T -> range
58978
e42da880c61e more position information, e.g. relevant for errors in generated ML source;
wenzelm
parents: 58854
diff changeset
    57
  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
    58
  val properties_of_range: range -> Properties.T
25817
d8e0190917a5 type T: based on properties, added id field;
wenzelm
parents: 25792
diff changeset
    59
  val thread_data: unit -> T
d8e0190917a5 type T: based on properties, added id field;
wenzelm
parents: 25792
diff changeset
    60
  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
    61
  val default: T -> bool * T
5010
9101b70b696d moved Thy/position.ML to General/position.ML;
wenzelm
parents:
diff changeset
    62
end;
9101b70b696d moved Thy/position.ML to General/position.ML;
wenzelm
parents:
diff changeset
    63
9101b70b696d moved Thy/position.ML to General/position.ML;
wenzelm
parents:
diff changeset
    64
structure Position: POSITION =
9101b70b696d moved Thy/position.ML to General/position.ML;
wenzelm
parents:
diff changeset
    65
struct
9101b70b696d moved Thy/position.ML to General/position.ML;
wenzelm
parents:
diff changeset
    66
9101b70b696d moved Thy/position.ML to General/position.ML;
wenzelm
parents:
diff changeset
    67
(* datatype position *)
9101b70b696d moved Thy/position.ML to General/position.ML;
wenzelm
parents:
diff changeset
    68
43710
7270ae921cf2 discontinued odd Position.column -- left-over from attempts at PGIP implementation;
wenzelm
parents: 42818
diff changeset
    69
datatype T = Pos of (int * int * int) * Properties.T;
41484
51310e1ccd6f more direct treatment of Position.end_offset;
wenzelm
parents: 41483
diff changeset
    70
51310e1ccd6f more direct treatment of Position.end_offset;
wenzelm
parents: 41483
diff changeset
    71
fun norm_props (props: Properties.T) =
45666
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45412
diff changeset
    72
  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
    73
    Markup.position_properties';
41484
51310e1ccd6f more direct treatment of Position.end_offset;
wenzelm
parents: 41483
diff changeset
    74
43710
7270ae921cf2 discontinued odd Position.column -- left-over from attempts at PGIP implementation;
wenzelm
parents: 42818
diff changeset
    75
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
    76
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
    77
27795
f67f4c677d81 count offset as well;
wenzelm
parents: 27791
diff changeset
    78
fun valid (i: int) = i > 0;
f67f4c677d81 count offset as well;
wenzelm
parents: 27791
diff changeset
    79
fun if_valid i i' = if valid i then i' else i;
f67f4c677d81 count offset as well;
wenzelm
parents: 27791
diff changeset
    80
27777
7a63d1b50b88 only increment column if valid;
wenzelm
parents: 27764
diff changeset
    81
27796
a6da5f68e776 added distance_of (permissive version);
wenzelm
parents: 27795
diff changeset
    82
(* fields *)
a6da5f68e776 added distance_of (permissive version);
wenzelm
parents: 27795
diff changeset
    83
43710
7270ae921cf2 discontinued odd Position.column -- left-over from attempts at PGIP implementation;
wenzelm
parents: 42818
diff changeset
    84
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
    85
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
    86
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
    87
50201
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49691
diff changeset
    88
fun file_of (Pos (_, props)) = Properties.get props Markup.fileN;
27796
a6da5f68e776 added distance_of (permissive version);
wenzelm
parents: 27795
diff changeset
    89
a6da5f68e776 added distance_of (permissive version);
wenzelm
parents: 27795
diff changeset
    90
27777
7a63d1b50b88 only increment column if valid;
wenzelm
parents: 27764
diff changeset
    91
(* advance *)
26003
7a8aee8353cf added column field;
wenzelm
parents: 25954
diff changeset
    92
43710
7270ae921cf2 discontinued odd Position.column -- left-over from attempts at PGIP implementation;
wenzelm
parents: 42818
diff changeset
    93
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
    94
      (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
    95
  | advance_count s (i, j, k) =
58854
b979c781c2db discontinued obsolete \<^sync> marker;
wenzelm
parents: 57899
diff changeset
    96
      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
    97
      else (i, j, k);
5010
9101b70b696d moved Thy/position.ML to General/position.ML;
wenzelm
parents:
diff changeset
    98
43710
7270ae921cf2 discontinued odd Position.column -- left-over from attempts at PGIP implementation;
wenzelm
parents: 42818
diff changeset
    99
fun invalid_count (i, j, _: int) =
7270ae921cf2 discontinued odd Position.column -- left-over from attempts at PGIP implementation;
wenzelm
parents: 42818
diff changeset
   100
  not (valid i orelse valid j);
27795
f67f4c677d81 count offset as well;
wenzelm
parents: 27791
diff changeset
   101
f67f4c677d81 count offset as well;
wenzelm
parents: 27791
diff changeset
   102
fun advance sym (pos as (Pos (count, props))) =
f67f4c677d81 count offset as well;
wenzelm
parents: 27791
diff changeset
   103
  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
   104
59085
08a6901eb035 clarified define_command: send tokens more directly, without requiring keywords in ML;
wenzelm
parents: 58978
diff changeset
   105
fun advance_offset offset (pos as (Pos (count as (i, j, k), props))) =
08a6901eb035 clarified define_command: send tokens more directly, without requiring keywords in ML;
wenzelm
parents: 58978
diff changeset
   106
  if invalid_count count then pos
08a6901eb035 clarified define_command: send tokens more directly, without requiring keywords in ML;
wenzelm
parents: 58978
diff changeset
   107
  else if valid i then raise Fail "Illegal line position"
08a6901eb035 clarified define_command: send tokens more directly, without requiring keywords in ML;
wenzelm
parents: 58978
diff changeset
   108
  else Pos ((i, if_valid j (j + offset), k), props);
08a6901eb035 clarified define_command: send tokens more directly, without requiring keywords in ML;
wenzelm
parents: 58978
diff changeset
   109
27777
7a63d1b50b88 only increment column if valid;
wenzelm
parents: 27764
diff changeset
   110
27796
a6da5f68e776 added distance_of (permissive version);
wenzelm
parents: 27795
diff changeset
   111
(* distance of adjacent positions *)
27777
7a63d1b50b88 only increment column if valid;
wenzelm
parents: 27764
diff changeset
   112
43710
7270ae921cf2 discontinued odd Position.column -- left-over from attempts at PGIP implementation;
wenzelm
parents: 42818
diff changeset
   113
fun distance_of (Pos ((_, j, _), _)) (Pos ((_, j', _), _)) =
27796
a6da5f68e776 added distance_of (permissive version);
wenzelm
parents: 27795
diff changeset
   114
  if valid j andalso valid j' then j' - j
a6da5f68e776 added distance_of (permissive version);
wenzelm
parents: 27795
diff changeset
   115
  else 0;
26882
9e824d8f4512 renamed Position.path to Path.position;
wenzelm
parents: 26633
diff changeset
   116
5010
9101b70b696d moved Thy/position.ML to General/position.ML;
wenzelm
parents:
diff changeset
   117
27777
7a63d1b50b88 only increment column if valid;
wenzelm
parents: 27764
diff changeset
   118
(* make position *)
7a63d1b50b88 only increment column if valid;
wenzelm
parents: 27764
diff changeset
   119
43710
7270ae921cf2 discontinued odd Position.column -- left-over from attempts at PGIP implementation;
wenzelm
parents: 42818
diff changeset
   120
val none = Pos ((0, 0, 0), []);
7270ae921cf2 discontinued odd Position.column -- left-over from attempts at PGIP implementation;
wenzelm
parents: 42818
diff changeset
   121
val start = Pos ((1, 1, 0), []);
27744
d4c5ddf98869 advance: operate on symbol list (less overhead);
wenzelm
parents: 27741
diff changeset
   122
29307
3a0b38b7fbb4 added id;
wenzelm
parents: 28122
diff changeset
   123
27796
a6da5f68e776 added distance_of (permissive version);
wenzelm
parents: 27795
diff changeset
   124
fun file_name "" = []
50201
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49691
diff changeset
   125
  | file_name name = [(Markup.fileN, name)];
27796
a6da5f68e776 added distance_of (permissive version);
wenzelm
parents: 27795
diff changeset
   126
44200
ce0112e26b3b tuned error message;
wenzelm
parents: 43710
diff changeset
   127
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
   128
fun file name = Pos ((1, 1, 0), file_name name);
27744
d4c5ddf98869 advance: operate on symbol list (less overhead);
wenzelm
parents: 27741
diff changeset
   129
56437
b14bd153a753 clarified position: no offset here;
wenzelm
parents: 56333
diff changeset
   130
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
   131
fun line_file i name = Pos ((i, 1, 0), file_name name);
27795
f67f4c677d81 count offset as well;
wenzelm
parents: 27791
diff changeset
   132
fun line i = line_file i "";
5010
9101b70b696d moved Thy/position.ML to General/position.ML;
wenzelm
parents:
diff changeset
   133
50201
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49691
diff changeset
   134
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
   135
fun id_only id = Pos ((0, 0, 0), [(Markup.idN, id)]);
22158
ff4fc4ee9eb0 Add line_of, name_of destructors.
aspinall
parents: 15531
diff changeset
   136
50201
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49691
diff changeset
   137
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
   138
fun put_id id (Pos (count, props)) = Pos (count, norm_props (Properties.put (Markup.idN, id) props));
27426
c0ef698c0904 added get_id/put_id;
wenzelm
parents: 26890
diff changeset
   139
50911
ee7fe4230642 more explicit treatment of (optional) exception properties, notably for "serial" -- avoid conflict with startPosition = offset;
wenzelm
parents: 50254
diff changeset
   140
fun parse_id pos = Option.map Markup.parse_int (get_id pos);
ee7fe4230642 more explicit treatment of (optional) exception properties, notably for "serial" -- avoid conflict with startPosition = offset;
wenzelm
parents: 50254
diff changeset
   141
29307
3a0b38b7fbb4 added id;
wenzelm
parents: 28122
diff changeset
   142
3a0b38b7fbb4 added id;
wenzelm
parents: 28122
diff changeset
   143
(* markup properties *)
3a0b38b7fbb4 added id;
wenzelm
parents: 28122
diff changeset
   144
58978
e42da880c61e more position information, e.g. relevant for errors in generated ML source;
wenzelm
parents: 58854
diff changeset
   145
fun get props name =
e42da880c61e more position information, e.g. relevant for errors in generated ML source;
wenzelm
parents: 58854
diff changeset
   146
  (case Properties.get props name of
e42da880c61e more position information, e.g. relevant for errors in generated ML source;
wenzelm
parents: 58854
diff changeset
   147
    NONE => 0
e42da880c61e more position information, e.g. relevant for errors in generated ML source;
wenzelm
parents: 58854
diff changeset
   148
  | SOME s => Markup.parse_int s);
e42da880c61e more position information, e.g. relevant for errors in generated ML source;
wenzelm
parents: 58854
diff changeset
   149
25817
d8e0190917a5 type T: based on properties, added id field;
wenzelm
parents: 25792
diff changeset
   150
fun of_properties props =
58978
e42da880c61e more position information, e.g. relevant for errors in generated ML source;
wenzelm
parents: 58854
diff changeset
   151
  make {line = get props Markup.lineN,
e42da880c61e more position information, e.g. relevant for errors in generated ML source;
wenzelm
parents: 58854
diff changeset
   152
    offset = get props Markup.offsetN,
e42da880c61e more position information, e.g. relevant for errors in generated ML source;
wenzelm
parents: 58854
diff changeset
   153
    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
   154
    props = props};
26003
7a8aee8353cf added column field;
wenzelm
parents: 25954
diff changeset
   155
50254
935ac0ad7e83 prefer tight Markup.print_int/parse_int for property values;
wenzelm
parents: 50201
diff changeset
   156
fun value k i = if valid i then [(k, Markup.print_int i)] else [];
41484
51310e1ccd6f more direct treatment of Position.end_offset;
wenzelm
parents: 41483
diff changeset
   157
43710
7270ae921cf2 discontinued odd Position.column -- left-over from attempts at PGIP implementation;
wenzelm
parents: 42818
diff changeset
   158
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
   159
  value Markup.lineN i @ value Markup.offsetN j @ value Markup.end_offsetN k @ props;
26003
7a8aee8353cf added column field;
wenzelm
parents: 25954
diff changeset
   160
54038
wenzelm
parents: 50911
diff changeset
   161
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
   162
57899
5867d1306712 clarified signature: entity serial number is not position id;
wenzelm
parents: 56532
diff changeset
   163
fun entity_properties_of def serial pos =
5867d1306712 clarified signature: entity serial number is not position id;
wenzelm
parents: 56532
diff changeset
   164
  if def then (Markup.defN, Markup.print_int serial) :: properties_of pos
5867d1306712 clarified signature: entity serial number is not position id;
wenzelm
parents: 56532
diff changeset
   165
  else (Markup.refN, Markup.print_int serial) :: def_properties_of pos;
45412
7797f5351ec4 entity markup for bound variables;
wenzelm
parents: 44736
diff changeset
   166
26052
7d5b3e34a735 added default_properties;
wenzelm
parents: 26003
diff changeset
   167
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
   168
  if exists (member (op =) Markup.position_properties o #1) props then props
26052
7d5b3e34a735 added default_properties;
wenzelm
parents: 26003
diff changeset
   169
  else properties_of default @ props;
7d5b3e34a735 added default_properties;
wenzelm
parents: 26003
diff changeset
   170
39440
4c2547af5909 simplified/clarified (Context_)Position.markup/reported_text;
wenzelm
parents: 38887
diff changeset
   171
val markup = Markup.properties o properties_of;
4c2547af5909 simplified/clarified (Context_)Position.markup/reported_text;
wenzelm
parents: 38887
diff changeset
   172
4c2547af5909 simplified/clarified (Context_)Position.markup/reported_text;
wenzelm
parents: 38887
diff changeset
   173
4c2547af5909 simplified/clarified (Context_)Position.markup/reported_text;
wenzelm
parents: 38887
diff changeset
   174
(* 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
   175
41504
f0f20a5b54df clarified notion Position.is_reported;
wenzelm
parents: 41484
diff changeset
   176
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
   177
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
   178
41504
f0f20a5b54df clarified notion Position.is_reported;
wenzelm
parents: 41484
diff changeset
   179
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
   180
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
   181
fun report pos markup = report_text pos markup "";
27764
e0ee3cc240fe advance: single argument (again);
wenzelm
parents: 27759
diff changeset
   182
44736
c2a3f1c84179 bulk reports for improved message throughput;
wenzelm
parents: 44735
diff changeset
   183
type report = T * Markup.T;
48767
7f0c469cc796 reports with body text, not just markup;
wenzelm
parents: 45666
diff changeset
   184
type report_text = report * string;
44736
c2a3f1c84179 bulk reports for improved message throughput;
wenzelm
parents: 44735
diff changeset
   185
48767
7f0c469cc796 reports with body text, not just markup;
wenzelm
parents: 45666
diff changeset
   186
val reports_text =
7f0c469cc796 reports with body text, not just markup;
wenzelm
parents: 45666
diff changeset
   187
  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
   188
  #> Output.report;
42204
b3277168c1e7 added Position.reports convenience;
wenzelm
parents: 41504
diff changeset
   189
48767
7f0c469cc796 reports with body text, not just markup;
wenzelm
parents: 45666
diff changeset
   190
val reports = map (rpair "") #> reports_text;
7f0c469cc796 reports with body text, not just markup;
wenzelm
parents: 45666
diff changeset
   191
44735
66862d02678c tuned signature;
wenzelm
parents: 44224
diff changeset
   192
fun store_reports _ [] _ _ = ()
55922
710bc66f432c more markup for inner syntax class/type names (notably for completion);
wenzelm
parents: 55624
diff changeset
   193
  | store_reports (r: report_text list Unsynchronized.ref) ps markup x =
42204
b3277168c1e7 added Position.reports convenience;
wenzelm
parents: 41504
diff changeset
   194
      let val ms = markup x
55922
710bc66f432c more markup for inner syntax class/type names (notably for completion);
wenzelm
parents: 55624
diff changeset
   195
      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
   196
55959
c3b458435f4f more decisive commitment to get_free vs. the_const;
wenzelm
parents: 55922
diff changeset
   197
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
   198
  Unsynchronized.change r (append (map (rpair "") reports));
c3b458435f4f more decisive commitment to get_free vs. the_const;
wenzelm
parents: 55922
diff changeset
   199
25817
d8e0190917a5 type T: based on properties, added id field;
wenzelm
parents: 25792
diff changeset
   200
56532
3da244bc02bd tuned message, to accommodate extra brackets produced by Scala parsers;
wenzelm
parents: 56459
diff changeset
   201
(* here: user output *)
26003
7a8aee8353cf added column field;
wenzelm
parents: 25954
diff changeset
   202
48992
0518bf89c777 renamed Position.str_of to Position.here;
wenzelm
parents: 48767
diff changeset
   203
fun here pos =
26003
7a8aee8353cf added column field;
wenzelm
parents: 25954
diff changeset
   204
  let
7a8aee8353cf added column field;
wenzelm
parents: 25954
diff changeset
   205
    val props = properties_of pos;
55624
d52409077135 tuned messages;
wenzelm
parents: 55546
diff changeset
   206
    val (s1, s2) =
26003
7a8aee8353cf added column field;
wenzelm
parents: 25954
diff changeset
   207
      (case (line_of pos, file_of pos) of
55624
d52409077135 tuned messages;
wenzelm
parents: 55546
diff changeset
   208
        (SOME i, NONE) => (" ", "(line " ^ Markup.print_int i ^ ")")
d52409077135 tuned messages;
wenzelm
parents: 55546
diff changeset
   209
      | (SOME i, SOME name) => (" ", "(line " ^ Markup.print_int i ^ " of " ^ quote name ^ ")")
d52409077135 tuned messages;
wenzelm
parents: 55546
diff changeset
   210
      | (NONE, SOME name) => (" ", "(file " ^ quote name ^ ")")
62529
8b7bdfc09f3b clarified treatment of fragments of Isabelle symbols during bootstrap;
wenzelm
parents: 59085
diff changeset
   211
      | _ => if is_reported pos then ("", "\<here>") else ("", ""));
26003
7a8aee8353cf added column field;
wenzelm
parents: 25954
diff changeset
   212
  in
7a8aee8353cf added column field;
wenzelm
parents: 25954
diff changeset
   213
    if null props then ""
55624
d52409077135 tuned messages;
wenzelm
parents: 55546
diff changeset
   214
    else s1 ^ Markup.markup (Markup.properties props Markup.position) s2
26003
7a8aee8353cf added column field;
wenzelm
parents: 25954
diff changeset
   215
  end;
25817
d8e0190917a5 type T: based on properties, added id field;
wenzelm
parents: 25792
diff changeset
   216
62803
5f73bf6ba98b required space is already part of Position.here;
wenzelm
parents: 62800
diff changeset
   217
val here_list = implode o map here;
49691
74ad6ecf2af2 more error positions;
wenzelm
parents: 49528
diff changeset
   218
23627
f543538866a2 added property conversions;
wenzelm
parents: 22158
diff changeset
   219
27736
3703dbd0cdea added encode_range;
wenzelm
parents: 27661
diff changeset
   220
(* range *)
3703dbd0cdea added encode_range;
wenzelm
parents: 27661
diff changeset
   221
3703dbd0cdea added encode_range;
wenzelm
parents: 27661
diff changeset
   222
type range = T * T;
3703dbd0cdea added encode_range;
wenzelm
parents: 27661
diff changeset
   223
27796
a6da5f68e776 added distance_of (permissive version);
wenzelm
parents: 27795
diff changeset
   224
val no_range = (none, none);
a6da5f68e776 added distance_of (permissive version);
wenzelm
parents: 27795
diff changeset
   225
62800
7ac100f86863 tuned signature;
wenzelm
parents: 62798
diff changeset
   226
fun no_range_position (Pos ((i, j, _), props)) = Pos ((i, j, 0), props);
62797
e08c44eed27f tuned signature;
wenzelm
parents: 62750
diff changeset
   227
fun range_position (Pos ((i, j, _), props), Pos ((_, j', _), _)) = Pos ((i, j, j'), props);
62800
7ac100f86863 tuned signature;
wenzelm
parents: 62798
diff changeset
   228
fun range (pos, pos') = (range_position (pos, pos'), no_range_position pos');
27777
7a63d1b50b88 only increment column if valid;
wenzelm
parents: 27764
diff changeset
   229
58978
e42da880c61e more position information, e.g. relevant for errors in generated ML source;
wenzelm
parents: 58854
diff changeset
   230
fun range_of_properties props =
e42da880c61e more position information, e.g. relevant for errors in generated ML source;
wenzelm
parents: 58854
diff changeset
   231
  let
e42da880c61e more position information, e.g. relevant for errors in generated ML source;
wenzelm
parents: 58854
diff changeset
   232
    val pos = of_properties props;
e42da880c61e more position information, e.g. relevant for errors in generated ML source;
wenzelm
parents: 58854
diff changeset
   233
    val pos' =
e42da880c61e more position information, e.g. relevant for errors in generated ML source;
wenzelm
parents: 58854
diff changeset
   234
      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
   235
        offset = get props Markup.end_offsetN,
e42da880c61e more position information, e.g. relevant for errors in generated ML source;
wenzelm
parents: 58854
diff changeset
   236
        end_offset = 0,
e42da880c61e more position information, e.g. relevant for errors in generated ML source;
wenzelm
parents: 58854
diff changeset
   237
        props = props};
e42da880c61e more position information, e.g. relevant for errors in generated ML source;
wenzelm
parents: 58854
diff changeset
   238
  in (pos, pos') end;
e42da880c61e more position information, e.g. relevant for errors in generated ML source;
wenzelm
parents: 58854
diff changeset
   239
e42da880c61e more position information, e.g. relevant for errors in generated ML source;
wenzelm
parents: 58854
diff changeset
   240
fun properties_of_range (pos, pos') =
e42da880c61e more position information, e.g. relevant for errors in generated ML source;
wenzelm
parents: 58854
diff changeset
   241
  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
   242
27764
e0ee3cc240fe advance: single argument (again);
wenzelm
parents: 27759
diff changeset
   243
e0ee3cc240fe advance: single argument (again);
wenzelm
parents: 27759
diff changeset
   244
(* thread data *)
e0ee3cc240fe advance: single argument (again);
wenzelm
parents: 27759
diff changeset
   245
62940
a03592aafadf tuned -- avoid recoding properties;
wenzelm
parents: 62929
diff changeset
   246
val thread_data = make o Thread_Position.get;
a03592aafadf tuned -- avoid recoding properties;
wenzelm
parents: 62929
diff changeset
   247
fun setmp_thread_data pos = Thread_Position.setmp (dest pos);
27764
e0ee3cc240fe advance: single argument (again);
wenzelm
parents: 27759
diff changeset
   248
33097
9d501e11084a maintain position of formal entities via name space;
wenzelm
parents: 32573
diff changeset
   249
fun default pos =
49528
789b73fcca72 report proper binding positions only -- avoid swamping document model with unspecific information;
wenzelm
parents: 48992
diff changeset
   250
  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
   251
  else (true, pos);
33097
9d501e11084a maintain position of formal entities via name space;
wenzelm
parents: 32573
diff changeset
   252
27764
e0ee3cc240fe advance: single argument (again);
wenzelm
parents: 27759
diff changeset
   253
end;