src/Pure/General/position.ML
author wenzelm
Wed, 16 Jan 2013 16:26:36 +0100
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;
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
43710
7270ae921cf2 discontinued odd Position.column -- left-over from attempts at PGIP implementation;
wenzelm
parents: 42818
diff changeset
    10
  val make: {line: int, offset: int, end_offset: int, props: Properties.T} -> T
7270ae921cf2 discontinued odd Position.column -- left-over from attempts at PGIP implementation;
wenzelm
parents: 42818
diff changeset
    11
  val dest: T -> {line: int, offset: int, end_offset: int, props: Properties.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
a6da5f68e776 added distance_of (permissive version);
wenzelm
parents: 27795
diff changeset
    17
  val distance_of: T -> T -> int
5010
9101b70b696d moved Thy/position.ML to General/position.ML;
wenzelm
parents:
diff changeset
    18
  val none: T
27777
7a63d1b50b88 only increment column if valid;
wenzelm
parents: 27764
diff changeset
    19
  val start: T
31435
d24ef3ff34bc export file_name;
wenzelm
parents: 31424
diff changeset
    20
  val file_name: string -> Properties.T
44200
ce0112e26b3b tuned error message;
wenzelm
parents: 43710
diff changeset
    21
  val file_only: string -> T
27777
7a63d1b50b88 only increment column if valid;
wenzelm
parents: 27764
diff changeset
    22
  val file: string -> T
5010
9101b70b696d moved Thy/position.ML to General/position.ML;
wenzelm
parents:
diff changeset
    23
  val line: int -> T
27777
7a63d1b50b88 only increment column if valid;
wenzelm
parents: 27764
diff changeset
    24
  val line_file: int -> string -> T
29307
3a0b38b7fbb4 added id;
wenzelm
parents: 28122
diff changeset
    25
  val id: string -> T
32573
62b5b538408d Isar.define_command: identify transaction;
wenzelm
parents: 32195
diff changeset
    26
  val id_only: string -> T
27426
c0ef698c0904 added get_id/put_id;
wenzelm
parents: 26890
diff changeset
    27
  val get_id: T -> string option
c0ef698c0904 added get_id/put_id;
wenzelm
parents: 26890
diff changeset
    28
  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
    29
  val parse_id: T -> int option
28017
4919bd124a58 type Properties.T;
wenzelm
parents: 27796
diff changeset
    30
  val of_properties: Properties.T -> T
4919bd124a58 type Properties.T;
wenzelm
parents: 27796
diff changeset
    31
  val properties_of: T -> Properties.T
42327
7c7cc7590eb3 Name_Space.entry_markup: keep def position as separate properties;
wenzelm
parents: 42204
diff changeset
    32
  val def_properties_of: T -> Properties.T
45412
7797f5351ec4 entity markup for bound variables;
wenzelm
parents: 44736
diff changeset
    33
  val entity_properties_of: bool -> serial -> T -> Properties.T
28017
4919bd124a58 type Properties.T;
wenzelm
parents: 27796
diff changeset
    34
  val default_properties: T -> Properties.T -> Properties.T
39440
4c2547af5909 simplified/clarified (Context_)Position.markup/reported_text;
wenzelm
parents: 38887
diff changeset
    35
  val markup: T -> Markup.T -> Markup.T
41504
f0f20a5b54df clarified notion Position.is_reported;
wenzelm
parents: 41484
diff changeset
    36
  val is_reported: T -> bool
39507
839873937ddd tuned signature of (Context_)Position.report variants;
wenzelm
parents: 39440
diff changeset
    37
  val reported_text: T -> Markup.T -> string -> string
839873937ddd tuned signature of (Context_)Position.report variants;
wenzelm
parents: 39440
diff changeset
    38
  val report_text: T -> Markup.T -> string -> unit
839873937ddd tuned signature of (Context_)Position.report variants;
wenzelm
parents: 39440
diff changeset
    39
  val report: T -> Markup.T -> unit
44736
c2a3f1c84179 bulk reports for improved message throughput;
wenzelm
parents: 44735
diff changeset
    40
  type report = T * Markup.T
48767
7f0c469cc796 reports with body text, not just markup;
wenzelm
parents: 45666
diff changeset
    41
  type report_text = report * string
7f0c469cc796 reports with body text, not just markup;
wenzelm
parents: 45666
diff changeset
    42
  val reports_text: report_text list -> unit
44736
c2a3f1c84179 bulk reports for improved message throughput;
wenzelm
parents: 44735
diff changeset
    43
  val reports: report list -> unit
c2a3f1c84179 bulk reports for improved message throughput;
wenzelm
parents: 44735
diff changeset
    44
  val store_reports: report list Unsynchronized.ref -> T list -> ('a -> Markup.T list) -> 'a -> unit
48992
0518bf89c777 renamed Position.str_of to Position.here;
wenzelm
parents: 48767
diff changeset
    45
  val here: T -> string
49691
74ad6ecf2af2 more error positions;
wenzelm
parents: 49528
diff changeset
    46
  val here_list: T list -> string
27764
e0ee3cc240fe advance: single argument (again);
wenzelm
parents: 27759
diff changeset
    47
  type range = T * T
27796
a6da5f68e776 added distance_of (permissive version);
wenzelm
parents: 27795
diff changeset
    48
  val no_range: range
41484
51310e1ccd6f more direct treatment of Position.end_offset;
wenzelm
parents: 41483
diff changeset
    49
  val set_range: range -> T
27777
7a63d1b50b88 only increment column if valid;
wenzelm
parents: 27764
diff changeset
    50
  val reset_range: T -> T
27764
e0ee3cc240fe advance: single argument (again);
wenzelm
parents: 27759
diff changeset
    51
  val range: T -> T -> range
25817
d8e0190917a5 type T: based on properties, added id field;
wenzelm
parents: 25792
diff changeset
    52
  val thread_data: unit -> T
d8e0190917a5 type T: based on properties, added id field;
wenzelm
parents: 25792
diff changeset
    53
  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
    54
  val default: T -> bool * T
5010
9101b70b696d moved Thy/position.ML to General/position.ML;
wenzelm
parents:
diff changeset
    55
end;
9101b70b696d moved Thy/position.ML to General/position.ML;
wenzelm
parents:
diff changeset
    56
9101b70b696d moved Thy/position.ML to General/position.ML;
wenzelm
parents:
diff changeset
    57
structure Position: POSITION =
9101b70b696d moved Thy/position.ML to General/position.ML;
wenzelm
parents:
diff changeset
    58
struct
9101b70b696d moved Thy/position.ML to General/position.ML;
wenzelm
parents:
diff changeset
    59
9101b70b696d moved Thy/position.ML to General/position.ML;
wenzelm
parents:
diff changeset
    60
(* datatype position *)
9101b70b696d moved Thy/position.ML to General/position.ML;
wenzelm
parents:
diff changeset
    61
43710
7270ae921cf2 discontinued odd Position.column -- left-over from attempts at PGIP implementation;
wenzelm
parents: 42818
diff changeset
    62
datatype T = Pos of (int * int * int) * Properties.T;
41484
51310e1ccd6f more direct treatment of Position.end_offset;
wenzelm
parents: 41483
diff changeset
    63
51310e1ccd6f more direct treatment of Position.end_offset;
wenzelm
parents: 41483
diff changeset
    64
fun norm_props (props: Properties.T) =
45666
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45412
diff changeset
    65
  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
    66
    Markup.position_properties';
41484
51310e1ccd6f more direct treatment of Position.end_offset;
wenzelm
parents: 41483
diff changeset
    67
43710
7270ae921cf2 discontinued odd Position.column -- left-over from attempts at PGIP implementation;
wenzelm
parents: 42818
diff changeset
    68
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
    69
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
    70
27795
f67f4c677d81 count offset as well;
wenzelm
parents: 27791
diff changeset
    71
fun valid (i: int) = i > 0;
f67f4c677d81 count offset as well;
wenzelm
parents: 27791
diff changeset
    72
fun if_valid i i' = if valid i then i' else i;
f67f4c677d81 count offset as well;
wenzelm
parents: 27791
diff changeset
    73
27777
7a63d1b50b88 only increment column if valid;
wenzelm
parents: 27764
diff changeset
    74
27796
a6da5f68e776 added distance_of (permissive version);
wenzelm
parents: 27795
diff changeset
    75
(* fields *)
a6da5f68e776 added distance_of (permissive version);
wenzelm
parents: 27795
diff changeset
    76
43710
7270ae921cf2 discontinued odd Position.column -- left-over from attempts at PGIP implementation;
wenzelm
parents: 42818
diff changeset
    77
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
    78
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
    79
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
    80
50201
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49691
diff changeset
    81
fun file_of (Pos (_, props)) = Properties.get props Markup.fileN;
27796
a6da5f68e776 added distance_of (permissive version);
wenzelm
parents: 27795
diff changeset
    82
a6da5f68e776 added distance_of (permissive version);
wenzelm
parents: 27795
diff changeset
    83
27777
7a63d1b50b88 only increment column if valid;
wenzelm
parents: 27764
diff changeset
    84
(* advance *)
26003
7a8aee8353cf added column field;
wenzelm
parents: 25954
diff changeset
    85
43710
7270ae921cf2 discontinued odd Position.column -- left-over from attempts at PGIP implementation;
wenzelm
parents: 42818
diff changeset
    86
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
    87
      (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
    88
  | advance_count s (i, j, k) =
7270ae921cf2 discontinued odd Position.column -- left-over from attempts at PGIP implementation;
wenzelm
parents: 42818
diff changeset
    89
      if Symbol.is_regular s then (i, if_valid j (j + 1), k)
7270ae921cf2 discontinued odd Position.column -- left-over from attempts at PGIP implementation;
wenzelm
parents: 42818
diff changeset
    90
      else (i, j, k);
5010
9101b70b696d moved Thy/position.ML to General/position.ML;
wenzelm
parents:
diff changeset
    91
43710
7270ae921cf2 discontinued odd Position.column -- left-over from attempts at PGIP implementation;
wenzelm
parents: 42818
diff changeset
    92
fun invalid_count (i, j, _: int) =
7270ae921cf2 discontinued odd Position.column -- left-over from attempts at PGIP implementation;
wenzelm
parents: 42818
diff changeset
    93
  not (valid i orelse valid j);
27795
f67f4c677d81 count offset as well;
wenzelm
parents: 27791
diff changeset
    94
f67f4c677d81 count offset as well;
wenzelm
parents: 27791
diff changeset
    95
fun advance sym (pos as (Pos (count, props))) =
f67f4c677d81 count offset as well;
wenzelm
parents: 27791
diff changeset
    96
  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
    97
7a63d1b50b88 only increment column if valid;
wenzelm
parents: 27764
diff changeset
    98
27796
a6da5f68e776 added distance_of (permissive version);
wenzelm
parents: 27795
diff changeset
    99
(* distance of adjacent positions *)
27777
7a63d1b50b88 only increment column if valid;
wenzelm
parents: 27764
diff changeset
   100
43710
7270ae921cf2 discontinued odd Position.column -- left-over from attempts at PGIP implementation;
wenzelm
parents: 42818
diff changeset
   101
fun distance_of (Pos ((_, j, _), _)) (Pos ((_, j', _), _)) =
27796
a6da5f68e776 added distance_of (permissive version);
wenzelm
parents: 27795
diff changeset
   102
  if valid j andalso valid j' then j' - j
a6da5f68e776 added distance_of (permissive version);
wenzelm
parents: 27795
diff changeset
   103
  else 0;
26882
9e824d8f4512 renamed Position.path to Path.position;
wenzelm
parents: 26633
diff changeset
   104
5010
9101b70b696d moved Thy/position.ML to General/position.ML;
wenzelm
parents:
diff changeset
   105
27777
7a63d1b50b88 only increment column if valid;
wenzelm
parents: 27764
diff changeset
   106
(* make position *)
7a63d1b50b88 only increment column if valid;
wenzelm
parents: 27764
diff changeset
   107
43710
7270ae921cf2 discontinued odd Position.column -- left-over from attempts at PGIP implementation;
wenzelm
parents: 42818
diff changeset
   108
val none = Pos ((0, 0, 0), []);
7270ae921cf2 discontinued odd Position.column -- left-over from attempts at PGIP implementation;
wenzelm
parents: 42818
diff changeset
   109
val start = Pos ((1, 1, 0), []);
27744
d4c5ddf98869 advance: operate on symbol list (less overhead);
wenzelm
parents: 27741
diff changeset
   110
29307
3a0b38b7fbb4 added id;
wenzelm
parents: 28122
diff changeset
   111
27796
a6da5f68e776 added distance_of (permissive version);
wenzelm
parents: 27795
diff changeset
   112
fun file_name "" = []
50201
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49691
diff changeset
   113
  | file_name name = [(Markup.fileN, name)];
27796
a6da5f68e776 added distance_of (permissive version);
wenzelm
parents: 27795
diff changeset
   114
44200
ce0112e26b3b tuned error message;
wenzelm
parents: 43710
diff changeset
   115
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
   116
fun file name = Pos ((1, 1, 0), file_name name);
27744
d4c5ddf98869 advance: operate on symbol list (less overhead);
wenzelm
parents: 27741
diff changeset
   117
43710
7270ae921cf2 discontinued odd Position.column -- left-over from attempts at PGIP implementation;
wenzelm
parents: 42818
diff changeset
   118
fun line_file i name = Pos ((i, 1, 0), file_name name);
27795
f67f4c677d81 count offset as well;
wenzelm
parents: 27791
diff changeset
   119
fun line i = line_file i "";
5010
9101b70b696d moved Thy/position.ML to General/position.ML;
wenzelm
parents:
diff changeset
   120
50201
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49691
diff changeset
   121
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
   122
fun id_only id = Pos ((0, 0, 0), [(Markup.idN, id)]);
22158
ff4fc4ee9eb0 Add line_of, name_of destructors.
aspinall
parents: 15531
diff changeset
   123
50201
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49691
diff changeset
   124
fun get_id (Pos (_, props)) = Properties.get props Markup.idN;
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49691
diff changeset
   125
fun put_id id (Pos (count, props)) = Pos (count, Properties.put (Markup.idN, id) props);
27426
c0ef698c0904 added get_id/put_id;
wenzelm
parents: 26890
diff changeset
   126
50911
ee7fe4230642 more explicit treatment of (optional) exception properties, notably for "serial" -- avoid conflict with startPosition = offset;
wenzelm
parents: 50254
diff changeset
   127
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
   128
29307
3a0b38b7fbb4 added id;
wenzelm
parents: 28122
diff changeset
   129
3a0b38b7fbb4 added id;
wenzelm
parents: 28122
diff changeset
   130
(* markup properties *)
3a0b38b7fbb4 added id;
wenzelm
parents: 28122
diff changeset
   131
25817
d8e0190917a5 type T: based on properties, added id field;
wenzelm
parents: 25792
diff changeset
   132
fun of_properties props =
23627
f543538866a2 added property conversions;
wenzelm
parents: 22158
diff changeset
   133
  let
27795
f67f4c677d81 count offset as well;
wenzelm
parents: 27791
diff changeset
   134
    fun get name =
28017
4919bd124a58 type Properties.T;
wenzelm
parents: 27796
diff changeset
   135
      (case Properties.get props name of
27795
f67f4c677d81 count offset as well;
wenzelm
parents: 27791
diff changeset
   136
        NONE => 0
50254
935ac0ad7e83 prefer tight Markup.print_int/parse_int for property values;
wenzelm
parents: 50201
diff changeset
   137
      | SOME s => Markup.parse_int s);
41484
51310e1ccd6f more direct treatment of Position.end_offset;
wenzelm
parents: 41483
diff changeset
   138
  in
50201
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49691
diff changeset
   139
    make {line = get Markup.lineN, offset = get Markup.offsetN,
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49691
diff changeset
   140
      end_offset = get Markup.end_offsetN, props = props}
41484
51310e1ccd6f more direct treatment of Position.end_offset;
wenzelm
parents: 41483
diff changeset
   141
  end;
51310e1ccd6f more direct treatment of Position.end_offset;
wenzelm
parents: 41483
diff changeset
   142
26003
7a8aee8353cf added column field;
wenzelm
parents: 25954
diff changeset
   143
50254
935ac0ad7e83 prefer tight Markup.print_int/parse_int for property values;
wenzelm
parents: 50201
diff changeset
   144
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
   145
43710
7270ae921cf2 discontinued odd Position.column -- left-over from attempts at PGIP implementation;
wenzelm
parents: 42818
diff changeset
   146
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
   147
  value Markup.lineN i @ value Markup.offsetN j @ value Markup.end_offsetN k @ props;
26003
7a8aee8353cf added column field;
wenzelm
parents: 25954
diff changeset
   148
42327
7c7cc7590eb3 Name_Space.entry_markup: keep def position as separate properties;
wenzelm
parents: 42204
diff changeset
   149
val def_properties_of = properties_of #> (map (fn (x, y) => ("def_" ^ x, y)));
7c7cc7590eb3 Name_Space.entry_markup: keep def position as separate properties;
wenzelm
parents: 42204
diff changeset
   150
45412
7797f5351ec4 entity markup for bound variables;
wenzelm
parents: 44736
diff changeset
   151
fun entity_properties_of def id pos =
50254
935ac0ad7e83 prefer tight Markup.print_int/parse_int for property values;
wenzelm
parents: 50201
diff changeset
   152
  if def then (Markup.defN, Markup.print_int id) :: properties_of pos
935ac0ad7e83 prefer tight Markup.print_int/parse_int for property values;
wenzelm
parents: 50201
diff changeset
   153
  else (Markup.refN, Markup.print_int id) :: def_properties_of pos;
45412
7797f5351ec4 entity markup for bound variables;
wenzelm
parents: 44736
diff changeset
   154
26052
7d5b3e34a735 added default_properties;
wenzelm
parents: 26003
diff changeset
   155
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
   156
  if exists (member (op =) Markup.position_properties o #1) props then props
26052
7d5b3e34a735 added default_properties;
wenzelm
parents: 26003
diff changeset
   157
  else properties_of default @ props;
7d5b3e34a735 added default_properties;
wenzelm
parents: 26003
diff changeset
   158
39440
4c2547af5909 simplified/clarified (Context_)Position.markup/reported_text;
wenzelm
parents: 38887
diff changeset
   159
val markup = Markup.properties o properties_of;
4c2547af5909 simplified/clarified (Context_)Position.markup/reported_text;
wenzelm
parents: 38887
diff changeset
   160
4c2547af5909 simplified/clarified (Context_)Position.markup/reported_text;
wenzelm
parents: 38887
diff changeset
   161
4c2547af5909 simplified/clarified (Context_)Position.markup/reported_text;
wenzelm
parents: 38887
diff changeset
   162
(* 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
   163
41504
f0f20a5b54df clarified notion Position.is_reported;
wenzelm
parents: 41484
diff changeset
   164
fun is_reported pos = is_some (offset_of pos) andalso is_some (get_id pos);
30669
6de7ef888aa3 added report_text -- status messages with text body;
wenzelm
parents: 29307
diff changeset
   165
41504
f0f20a5b54df clarified notion Position.is_reported;
wenzelm
parents: 41484
diff changeset
   166
fun reported_text pos m txt = if is_reported pos then Markup.markup (markup pos m) txt else "";
39507
839873937ddd tuned signature of (Context_)Position.report variants;
wenzelm
parents: 39440
diff changeset
   167
fun report_text pos markup txt = Output.report (reported_text pos markup txt);
839873937ddd tuned signature of (Context_)Position.report variants;
wenzelm
parents: 39440
diff changeset
   168
fun report pos markup = report_text pos markup "";
27764
e0ee3cc240fe advance: single argument (again);
wenzelm
parents: 27759
diff changeset
   169
44736
c2a3f1c84179 bulk reports for improved message throughput;
wenzelm
parents: 44735
diff changeset
   170
type report = T * Markup.T;
48767
7f0c469cc796 reports with body text, not just markup;
wenzelm
parents: 45666
diff changeset
   171
type report_text = report * string;
44736
c2a3f1c84179 bulk reports for improved message throughput;
wenzelm
parents: 44735
diff changeset
   172
48767
7f0c469cc796 reports with body text, not just markup;
wenzelm
parents: 45666
diff changeset
   173
val reports_text =
7f0c469cc796 reports with body text, not just markup;
wenzelm
parents: 45666
diff changeset
   174
  map (fn ((pos, m), txt) => if is_reported pos then Markup.markup (markup pos m) txt else "")
44736
c2a3f1c84179 bulk reports for improved message throughput;
wenzelm
parents: 44735
diff changeset
   175
  #> implode #> Output.report;
42204
b3277168c1e7 added Position.reports convenience;
wenzelm
parents: 41504
diff changeset
   176
48767
7f0c469cc796 reports with body text, not just markup;
wenzelm
parents: 45666
diff changeset
   177
val reports = map (rpair "") #> reports_text;
7f0c469cc796 reports with body text, not just markup;
wenzelm
parents: 45666
diff changeset
   178
44735
66862d02678c tuned signature;
wenzelm
parents: 44224
diff changeset
   179
fun store_reports _ [] _ _ = ()
44736
c2a3f1c84179 bulk reports for improved message throughput;
wenzelm
parents: 44735
diff changeset
   180
  | store_reports (r: report list Unsynchronized.ref) ps markup x =
42204
b3277168c1e7 added Position.reports convenience;
wenzelm
parents: 41504
diff changeset
   181
      let val ms = markup x
b3277168c1e7 added Position.reports convenience;
wenzelm
parents: 41504
diff changeset
   182
      in Unsynchronized.change r (fold (fn p => fold (fn m => cons (p, m)) ms) ps) end;
b3277168c1e7 added Position.reports convenience;
wenzelm
parents: 41504
diff changeset
   183
25817
d8e0190917a5 type T: based on properties, added id field;
wenzelm
parents: 25792
diff changeset
   184
48992
0518bf89c777 renamed Position.str_of to Position.here;
wenzelm
parents: 48767
diff changeset
   185
(* here: inlined formal markup *)
26003
7a8aee8353cf added column field;
wenzelm
parents: 25954
diff changeset
   186
48992
0518bf89c777 renamed Position.str_of to Position.here;
wenzelm
parents: 48767
diff changeset
   187
fun here pos =
26003
7a8aee8353cf added column field;
wenzelm
parents: 25954
diff changeset
   188
  let
7a8aee8353cf added column field;
wenzelm
parents: 25954
diff changeset
   189
    val props = properties_of pos;
7a8aee8353cf added column field;
wenzelm
parents: 25954
diff changeset
   190
    val s =
7a8aee8353cf added column field;
wenzelm
parents: 25954
diff changeset
   191
      (case (line_of pos, file_of pos) of
50254
935ac0ad7e83 prefer tight Markup.print_int/parse_int for property values;
wenzelm
parents: 50201
diff changeset
   192
        (SOME i, NONE) => "(line " ^ Markup.print_int i ^ ")"
935ac0ad7e83 prefer tight Markup.print_int/parse_int for property values;
wenzelm
parents: 50201
diff changeset
   193
      | (SOME i, SOME name) => "(line " ^ Markup.print_int i ^ " of " ^ quote name ^ ")"
44224
4040d0ffac7b tuned message;
wenzelm
parents: 44200
diff changeset
   194
      | (NONE, SOME name) => "(file " ^ quote name ^ ")"
26003
7a8aee8353cf added column field;
wenzelm
parents: 25954
diff changeset
   195
      | _ => "");
7a8aee8353cf added column field;
wenzelm
parents: 25954
diff changeset
   196
  in
7a8aee8353cf added column field;
wenzelm
parents: 25954
diff changeset
   197
    if null props then ""
50201
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 49691
diff changeset
   198
    else (if s = "" then "" else " ") ^ Markup.markup (Markup.properties props Markup.position) s
26003
7a8aee8353cf added column field;
wenzelm
parents: 25954
diff changeset
   199
  end;
25817
d8e0190917a5 type T: based on properties, added id field;
wenzelm
parents: 25792
diff changeset
   200
49691
74ad6ecf2af2 more error positions;
wenzelm
parents: 49528
diff changeset
   201
val here_list = space_implode " " o map here;
74ad6ecf2af2 more error positions;
wenzelm
parents: 49528
diff changeset
   202
23627
f543538866a2 added property conversions;
wenzelm
parents: 22158
diff changeset
   203
27736
3703dbd0cdea added encode_range;
wenzelm
parents: 27661
diff changeset
   204
(* range *)
3703dbd0cdea added encode_range;
wenzelm
parents: 27661
diff changeset
   205
3703dbd0cdea added encode_range;
wenzelm
parents: 27661
diff changeset
   206
type range = T * T;
3703dbd0cdea added encode_range;
wenzelm
parents: 27661
diff changeset
   207
27796
a6da5f68e776 added distance_of (permissive version);
wenzelm
parents: 27795
diff changeset
   208
val no_range = (none, none);
a6da5f68e776 added distance_of (permissive version);
wenzelm
parents: 27795
diff changeset
   209
43710
7270ae921cf2 discontinued odd Position.column -- left-over from attempts at PGIP implementation;
wenzelm
parents: 42818
diff changeset
   210
fun set_range (Pos ((i, j, _), props), Pos ((_, j', _), _)) = Pos ((i, j, j'), props);
7270ae921cf2 discontinued odd Position.column -- left-over from attempts at PGIP implementation;
wenzelm
parents: 42818
diff changeset
   211
fun reset_range (Pos ((i, j, _), props)) = Pos ((i, j, 0), props);
27777
7a63d1b50b88 only increment column if valid;
wenzelm
parents: 27764
diff changeset
   212
41484
51310e1ccd6f more direct treatment of Position.end_offset;
wenzelm
parents: 41483
diff changeset
   213
fun range pos pos' = (set_range (pos, pos'), pos');
27741
d2523b72ed44 added report;
wenzelm
parents: 27736
diff changeset
   214
27764
e0ee3cc240fe advance: single argument (again);
wenzelm
parents: 27759
diff changeset
   215
e0ee3cc240fe advance: single argument (again);
wenzelm
parents: 27759
diff changeset
   216
(* thread data *)
e0ee3cc240fe advance: single argument (again);
wenzelm
parents: 27759
diff changeset
   217
e0ee3cc240fe advance: single argument (again);
wenzelm
parents: 27759
diff changeset
   218
local val tag = Universal.tag () : T Universal.tag in
27741
d2523b72ed44 added report;
wenzelm
parents: 27736
diff changeset
   219
28122
3d099ce624e7 Thread.getLocal/setLocal;
wenzelm
parents: 28017
diff changeset
   220
fun thread_data () = the_default none (Thread.getLocal tag);
27764
e0ee3cc240fe advance: single argument (again);
wenzelm
parents: 27759
diff changeset
   221
37043
f8e24980af05 more robust Position.setmp_thread_data, independently of Output.debugging (essentially reverts f9ec18f7c0f6, which was motivated by clean exception_trace, but without transaction positions the Isabelle_Process protocol breaks down);
wenzelm
parents: 33097
diff changeset
   222
fun setmp_thread_data pos = Library.setmp_thread_data tag (thread_data ()) pos;
27764
e0ee3cc240fe advance: single argument (again);
wenzelm
parents: 27759
diff changeset
   223
5010
9101b70b696d moved Thy/position.ML to General/position.ML;
wenzelm
parents:
diff changeset
   224
end;
27764
e0ee3cc240fe advance: single argument (again);
wenzelm
parents: 27759
diff changeset
   225
33097
9d501e11084a maintain position of formal entities via name space;
wenzelm
parents: 32573
diff changeset
   226
fun default pos =
49528
789b73fcca72 report proper binding positions only -- avoid swamping document model with unspecific information;
wenzelm
parents: 48992
diff changeset
   227
  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
   228
  else (true, pos);
33097
9d501e11084a maintain position of formal entities via name space;
wenzelm
parents: 32573
diff changeset
   229
27764
e0ee3cc240fe advance: single argument (again);
wenzelm
parents: 27759
diff changeset
   230
end;