src/Pure/General/position.ML
author haftmann
Tue, 23 Sep 2008 18:11:44 +0200
changeset 28337 93964076e7b8
parent 28122 3d099ce624e7
child 29307 3a0b38b7fbb4
permissions -rw-r--r--
case default fallback for NBE
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
    ID:         $Id$
9101b70b696d moved Thy/position.ML to General/position.ML;
wenzelm
parents:
diff changeset
     3
    Author:     Markus Wenzel, TU Muenchen
9101b70b696d moved Thy/position.ML to General/position.ML;
wenzelm
parents:
diff changeset
     4
27795
f67f4c677d81 count offset as well;
wenzelm
parents: 27791
diff changeset
     5
Source positions: counting Isabelle symbols -- starting from 1.
5010
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
9101b70b696d moved Thy/position.ML to General/position.ML;
wenzelm
parents:
diff changeset
     8
signature POSITION =
9101b70b696d moved Thy/position.ML to General/position.ML;
wenzelm
parents:
diff changeset
     9
sig
9101b70b696d moved Thy/position.ML to General/position.ML;
wenzelm
parents:
diff changeset
    10
  type T
23673
67c748e5ae54 replaced name by file (unquoted);
wenzelm
parents: 23627
diff changeset
    11
  val line_of: T -> int option
26003
7a8aee8353cf added column field;
wenzelm
parents: 25954
diff changeset
    12
  val column_of: T -> int option
27795
f67f4c677d81 count offset as well;
wenzelm
parents: 27791
diff changeset
    13
  val offset_of: T -> int option
23673
67c748e5ae54 replaced name by file (unquoted);
wenzelm
parents: 23627
diff changeset
    14
  val file_of: T -> string option
27796
a6da5f68e776 added distance_of (permissive version);
wenzelm
parents: 27795
diff changeset
    15
  val advance: Symbol.symbol -> T -> T
a6da5f68e776 added distance_of (permissive version);
wenzelm
parents: 27795
diff changeset
    16
  val distance_of: T -> T -> int
5010
9101b70b696d moved Thy/position.ML to General/position.ML;
wenzelm
parents:
diff changeset
    17
  val none: T
27777
7a63d1b50b88 only increment column if valid;
wenzelm
parents: 27764
diff changeset
    18
  val start: T
7a63d1b50b88 only increment column if valid;
wenzelm
parents: 27764
diff changeset
    19
  val file: string -> T
5010
9101b70b696d moved Thy/position.ML to General/position.ML;
wenzelm
parents:
diff changeset
    20
  val line: int -> T
27777
7a63d1b50b88 only increment column if valid;
wenzelm
parents: 27764
diff changeset
    21
  val line_file: int -> string -> T
27426
c0ef698c0904 added get_id/put_id;
wenzelm
parents: 26890
diff changeset
    22
  val get_id: T -> string option
c0ef698c0904 added get_id/put_id;
wenzelm
parents: 26890
diff changeset
    23
  val put_id: string -> T -> T
28017
4919bd124a58 type Properties.T;
wenzelm
parents: 27796
diff changeset
    24
  val of_properties: Properties.T -> T
4919bd124a58 type Properties.T;
wenzelm
parents: 27796
diff changeset
    25
  val properties_of: T -> Properties.T
4919bd124a58 type Properties.T;
wenzelm
parents: 27796
diff changeset
    26
  val default_properties: T -> Properties.T -> Properties.T
27764
e0ee3cc240fe advance: single argument (again);
wenzelm
parents: 27759
diff changeset
    27
  val report: Markup.T -> T -> unit
26003
7a8aee8353cf added column field;
wenzelm
parents: 25954
diff changeset
    28
  val str_of: T -> string
27764
e0ee3cc240fe advance: single argument (again);
wenzelm
parents: 27759
diff changeset
    29
  type range = T * T
27796
a6da5f68e776 added distance_of (permissive version);
wenzelm
parents: 27795
diff changeset
    30
  val no_range: range
27764
e0ee3cc240fe advance: single argument (again);
wenzelm
parents: 27759
diff changeset
    31
  val encode_range: range -> T
27777
7a63d1b50b88 only increment column if valid;
wenzelm
parents: 27764
diff changeset
    32
  val reset_range: T -> T
27764
e0ee3cc240fe advance: single argument (again);
wenzelm
parents: 27759
diff changeset
    33
  val range: T -> T -> range
25817
d8e0190917a5 type T: based on properties, added id field;
wenzelm
parents: 25792
diff changeset
    34
  val thread_data: unit -> T
d8e0190917a5 type T: based on properties, added id field;
wenzelm
parents: 25792
diff changeset
    35
  val setmp_thread_data: T -> ('a -> 'b) -> 'a -> 'b
25954
682e84b60e5c added setmp_thread_data_seq;
wenzelm
parents: 25817
diff changeset
    36
  val setmp_thread_data_seq: T -> ('a -> 'b Seq.seq) -> 'a -> 'b Seq.seq
5010
9101b70b696d moved Thy/position.ML to General/position.ML;
wenzelm
parents:
diff changeset
    37
end;
9101b70b696d moved Thy/position.ML to General/position.ML;
wenzelm
parents:
diff changeset
    38
9101b70b696d moved Thy/position.ML to General/position.ML;
wenzelm
parents:
diff changeset
    39
structure Position: POSITION =
9101b70b696d moved Thy/position.ML to General/position.ML;
wenzelm
parents:
diff changeset
    40
struct
9101b70b696d moved Thy/position.ML to General/position.ML;
wenzelm
parents:
diff changeset
    41
9101b70b696d moved Thy/position.ML to General/position.ML;
wenzelm
parents:
diff changeset
    42
(* datatype position *)
9101b70b696d moved Thy/position.ML to General/position.ML;
wenzelm
parents:
diff changeset
    43
28017
4919bd124a58 type Properties.T;
wenzelm
parents: 27796
diff changeset
    44
datatype T = Pos of (int * int * int) * Properties.T;
27777
7a63d1b50b88 only increment column if valid;
wenzelm
parents: 27764
diff changeset
    45
27795
f67f4c677d81 count offset as well;
wenzelm
parents: 27791
diff changeset
    46
fun valid (i: int) = i > 0;
f67f4c677d81 count offset as well;
wenzelm
parents: 27791
diff changeset
    47
fun if_valid i i' = if valid i then i' else i;
f67f4c677d81 count offset as well;
wenzelm
parents: 27791
diff changeset
    48
f67f4c677d81 count offset as well;
wenzelm
parents: 27791
diff changeset
    49
fun value k i = if valid i then [(k, string_of_int i)] else [];
27777
7a63d1b50b88 only increment column if valid;
wenzelm
parents: 27764
diff changeset
    50
7a63d1b50b88 only increment column if valid;
wenzelm
parents: 27764
diff changeset
    51
27796
a6da5f68e776 added distance_of (permissive version);
wenzelm
parents: 27795
diff changeset
    52
(* fields *)
a6da5f68e776 added distance_of (permissive version);
wenzelm
parents: 27795
diff changeset
    53
a6da5f68e776 added distance_of (permissive version);
wenzelm
parents: 27795
diff changeset
    54
fun line_of (Pos ((i, _, _), _)) = if valid i then SOME i else NONE;
a6da5f68e776 added distance_of (permissive version);
wenzelm
parents: 27795
diff changeset
    55
fun column_of (Pos ((_, j, _), _)) = if valid j then SOME j else NONE;
a6da5f68e776 added distance_of (permissive version);
wenzelm
parents: 27795
diff changeset
    56
fun offset_of (Pos ((_, _, k), _)) = if valid k then SOME k else NONE;
a6da5f68e776 added distance_of (permissive version);
wenzelm
parents: 27795
diff changeset
    57
28017
4919bd124a58 type Properties.T;
wenzelm
parents: 27796
diff changeset
    58
fun file_of (Pos (_, props)) = Properties.get props Markup.fileN;
27796
a6da5f68e776 added distance_of (permissive version);
wenzelm
parents: 27795
diff changeset
    59
a6da5f68e776 added distance_of (permissive version);
wenzelm
parents: 27795
diff changeset
    60
27777
7a63d1b50b88 only increment column if valid;
wenzelm
parents: 27764
diff changeset
    61
(* advance *)
26003
7a8aee8353cf added column field;
wenzelm
parents: 25954
diff changeset
    62
27795
f67f4c677d81 count offset as well;
wenzelm
parents: 27791
diff changeset
    63
fun advance_count "\n" (i: int, j: int, k: int) =
f67f4c677d81 count offset as well;
wenzelm
parents: 27791
diff changeset
    64
      (if_valid i (i + 1), if_valid j 1, if_valid k (k + 1))
f67f4c677d81 count offset as well;
wenzelm
parents: 27791
diff changeset
    65
  | advance_count s (i, j, k) =
f67f4c677d81 count offset as well;
wenzelm
parents: 27791
diff changeset
    66
      if Symbol.is_regular s andalso not (Symbol.is_utf8_trailer s)
f67f4c677d81 count offset as well;
wenzelm
parents: 27791
diff changeset
    67
      then (i, if_valid j (j + 1), if_valid k (k + 1)) else (i, j, k);
5010
9101b70b696d moved Thy/position.ML to General/position.ML;
wenzelm
parents:
diff changeset
    68
27795
f67f4c677d81 count offset as well;
wenzelm
parents: 27791
diff changeset
    69
fun invalid_count (i, j, k) =
f67f4c677d81 count offset as well;
wenzelm
parents: 27791
diff changeset
    70
  not (valid i orelse valid j orelse valid k);
f67f4c677d81 count offset as well;
wenzelm
parents: 27791
diff changeset
    71
f67f4c677d81 count offset as well;
wenzelm
parents: 27791
diff changeset
    72
fun advance sym (pos as (Pos (count, props))) =
f67f4c677d81 count offset as well;
wenzelm
parents: 27791
diff changeset
    73
  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
    74
7a63d1b50b88 only increment column if valid;
wenzelm
parents: 27764
diff changeset
    75
27796
a6da5f68e776 added distance_of (permissive version);
wenzelm
parents: 27795
diff changeset
    76
(* distance of adjacent positions *)
27777
7a63d1b50b88 only increment column if valid;
wenzelm
parents: 27764
diff changeset
    77
27796
a6da5f68e776 added distance_of (permissive version);
wenzelm
parents: 27795
diff changeset
    78
fun distance_of (Pos ((_, j, k), _)) (Pos ((_, j', k'), _)) =
a6da5f68e776 added distance_of (permissive version);
wenzelm
parents: 27795
diff changeset
    79
  if valid j andalso valid j' then j' - j
a6da5f68e776 added distance_of (permissive version);
wenzelm
parents: 27795
diff changeset
    80
  else if valid k andalso valid k' then k' - k
a6da5f68e776 added distance_of (permissive version);
wenzelm
parents: 27795
diff changeset
    81
  else 0;
26882
9e824d8f4512 renamed Position.path to Path.position;
wenzelm
parents: 26633
diff changeset
    82
5010
9101b70b696d moved Thy/position.ML to General/position.ML;
wenzelm
parents:
diff changeset
    83
27777
7a63d1b50b88 only increment column if valid;
wenzelm
parents: 27764
diff changeset
    84
(* make position *)
7a63d1b50b88 only increment column if valid;
wenzelm
parents: 27764
diff changeset
    85
27795
f67f4c677d81 count offset as well;
wenzelm
parents: 27791
diff changeset
    86
val none = Pos ((0, 0, 0), []);
f67f4c677d81 count offset as well;
wenzelm
parents: 27791
diff changeset
    87
val start = Pos ((1, 1, 1), []);
27744
d4c5ddf98869 advance: operate on symbol list (less overhead);
wenzelm
parents: 27741
diff changeset
    88
27796
a6da5f68e776 added distance_of (permissive version);
wenzelm
parents: 27795
diff changeset
    89
fun file_name "" = []
a6da5f68e776 added distance_of (permissive version);
wenzelm
parents: 27795
diff changeset
    90
  | file_name name = [(Markup.fileN, name)];
a6da5f68e776 added distance_of (permissive version);
wenzelm
parents: 27795
diff changeset
    91
27795
f67f4c677d81 count offset as well;
wenzelm
parents: 27791
diff changeset
    92
fun file name = Pos ((1, 1, 1), file_name name);
27744
d4c5ddf98869 advance: operate on symbol list (less overhead);
wenzelm
parents: 27741
diff changeset
    93
27795
f67f4c677d81 count offset as well;
wenzelm
parents: 27791
diff changeset
    94
fun line_file i name = Pos ((i, 0, 0), file_name name);
f67f4c677d81 count offset as well;
wenzelm
parents: 27791
diff changeset
    95
fun line i = line_file i "";
5010
9101b70b696d moved Thy/position.ML to General/position.ML;
wenzelm
parents:
diff changeset
    96
23627
f543538866a2 added property conversions;
wenzelm
parents: 22158
diff changeset
    97
f543538866a2 added property conversions;
wenzelm
parents: 22158
diff changeset
    98
(* markup properties *)
22158
ff4fc4ee9eb0 Add line_of, name_of destructors.
aspinall
parents: 15531
diff changeset
    99
28017
4919bd124a58 type Properties.T;
wenzelm
parents: 27796
diff changeset
   100
fun get_id (Pos (_, props)) = Properties.get props Markup.idN;
4919bd124a58 type Properties.T;
wenzelm
parents: 27796
diff changeset
   101
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
   102
25817
d8e0190917a5 type T: based on properties, added id field;
wenzelm
parents: 25792
diff changeset
   103
fun of_properties props =
23627
f543538866a2 added property conversions;
wenzelm
parents: 22158
diff changeset
   104
  let
27795
f67f4c677d81 count offset as well;
wenzelm
parents: 27791
diff changeset
   105
    fun get name =
28017
4919bd124a58 type Properties.T;
wenzelm
parents: 27796
diff changeset
   106
      (case Properties.get props name of
27795
f67f4c677d81 count offset as well;
wenzelm
parents: 27791
diff changeset
   107
        NONE => 0
f67f4c677d81 count offset as well;
wenzelm
parents: 27791
diff changeset
   108
      | SOME s => the_default 0 (Int.fromString s));
f67f4c677d81 count offset as well;
wenzelm
parents: 27791
diff changeset
   109
    val count = (get Markup.lineN, get Markup.columnN, get Markup.offsetN);
26003
7a8aee8353cf added column field;
wenzelm
parents: 25954
diff changeset
   110
    fun property name = the_list (find_first (fn (x: string, _) => x = name) props);
27749
24f2b57a34ea of_properties: observe Markup.position_properties';
wenzelm
parents: 27744
diff changeset
   111
  in Pos (count, maps property Markup.position_properties') end;
26003
7a8aee8353cf added column field;
wenzelm
parents: 25954
diff changeset
   112
27795
f67f4c677d81 count offset as well;
wenzelm
parents: 27791
diff changeset
   113
fun properties_of (Pos ((i, j, k), props)) =
f67f4c677d81 count offset as well;
wenzelm
parents: 27791
diff changeset
   114
  value Markup.lineN i @ value Markup.columnN j @ value Markup.offsetN k @ props;
26003
7a8aee8353cf added column field;
wenzelm
parents: 25954
diff changeset
   115
26052
7d5b3e34a735 added default_properties;
wenzelm
parents: 26003
diff changeset
   116
fun default_properties default props =
7d5b3e34a735 added default_properties;
wenzelm
parents: 26003
diff changeset
   117
  if exists (member (op =) Markup.position_properties o #1) props then props
7d5b3e34a735 added default_properties;
wenzelm
parents: 26003
diff changeset
   118
  else properties_of default @ props;
7d5b3e34a735 added default_properties;
wenzelm
parents: 26003
diff changeset
   119
27795
f67f4c677d81 count offset as well;
wenzelm
parents: 27791
diff changeset
   120
fun report markup (pos as Pos (count, _)) =
f67f4c677d81 count offset as well;
wenzelm
parents: 27791
diff changeset
   121
  if invalid_count count then ()
27764
e0ee3cc240fe advance: single argument (again);
wenzelm
parents: 27759
diff changeset
   122
  else Output.status (Markup.markup (Markup.properties (properties_of pos) markup) "");
e0ee3cc240fe advance: single argument (again);
wenzelm
parents: 27759
diff changeset
   123
25817
d8e0190917a5 type T: based on properties, added id field;
wenzelm
parents: 25792
diff changeset
   124
26003
7a8aee8353cf added column field;
wenzelm
parents: 25954
diff changeset
   125
(* str_of *)
7a8aee8353cf added column field;
wenzelm
parents: 25954
diff changeset
   126
7a8aee8353cf added column field;
wenzelm
parents: 25954
diff changeset
   127
fun str_of pos =
7a8aee8353cf added column field;
wenzelm
parents: 25954
diff changeset
   128
  let
7a8aee8353cf added column field;
wenzelm
parents: 25954
diff changeset
   129
    val props = properties_of pos;
7a8aee8353cf added column field;
wenzelm
parents: 25954
diff changeset
   130
    val s =
7a8aee8353cf added column field;
wenzelm
parents: 25954
diff changeset
   131
      (case (line_of pos, file_of pos) of
27795
f67f4c677d81 count offset as well;
wenzelm
parents: 27791
diff changeset
   132
        (SOME i, NONE) => "(line " ^ string_of_int i ^ ")"
f67f4c677d81 count offset as well;
wenzelm
parents: 27791
diff changeset
   133
      | (SOME i, SOME name) => "(line " ^ string_of_int i ^ " of " ^ quote name ^ ")"
26003
7a8aee8353cf added column field;
wenzelm
parents: 25954
diff changeset
   134
      | _ => "");
7a8aee8353cf added column field;
wenzelm
parents: 25954
diff changeset
   135
  in
7a8aee8353cf added column field;
wenzelm
parents: 25954
diff changeset
   136
    if null props then ""
7a8aee8353cf added column field;
wenzelm
parents: 25954
diff changeset
   137
    else (if s = "" then "" else " ") ^ Markup.markup (Markup.properties props Markup.position) s
7a8aee8353cf added column field;
wenzelm
parents: 25954
diff changeset
   138
  end;
25817
d8e0190917a5 type T: based on properties, added id field;
wenzelm
parents: 25792
diff changeset
   139
23627
f543538866a2 added property conversions;
wenzelm
parents: 22158
diff changeset
   140
27736
3703dbd0cdea added encode_range;
wenzelm
parents: 27661
diff changeset
   141
(* range *)
3703dbd0cdea added encode_range;
wenzelm
parents: 27661
diff changeset
   142
3703dbd0cdea added encode_range;
wenzelm
parents: 27661
diff changeset
   143
type range = T * T;
3703dbd0cdea added encode_range;
wenzelm
parents: 27661
diff changeset
   144
27796
a6da5f68e776 added distance_of (permissive version);
wenzelm
parents: 27795
diff changeset
   145
val no_range = (none, none);
a6da5f68e776 added distance_of (permissive version);
wenzelm
parents: 27795
diff changeset
   146
27795
f67f4c677d81 count offset as well;
wenzelm
parents: 27791
diff changeset
   147
fun encode_range (Pos (count, props), Pos ((i, j, k), _)) =
28017
4919bd124a58 type Properties.T;
wenzelm
parents: 27796
diff changeset
   148
  let val props' = props |> fold_rev Properties.put
27795
f67f4c677d81 count offset as well;
wenzelm
parents: 27791
diff changeset
   149
    (value Markup.end_lineN i @ value Markup.end_columnN j @ value Markup.end_offsetN k)
f67f4c677d81 count offset as well;
wenzelm
parents: 27791
diff changeset
   150
  in Pos (count, props') end;
27777
7a63d1b50b88 only increment column if valid;
wenzelm
parents: 27764
diff changeset
   151
7a63d1b50b88 only increment column if valid;
wenzelm
parents: 27764
diff changeset
   152
fun reset_range (Pos (count, props)) =
28017
4919bd124a58 type Properties.T;
wenzelm
parents: 27796
diff changeset
   153
  let val props' = props |> fold Properties.remove
27795
f67f4c677d81 count offset as well;
wenzelm
parents: 27791
diff changeset
   154
    [Markup.end_lineN, Markup.end_columnN, Markup.end_offsetN]
f67f4c677d81 count offset as well;
wenzelm
parents: 27791
diff changeset
   155
  in Pos (count, props') end;
27736
3703dbd0cdea added encode_range;
wenzelm
parents: 27661
diff changeset
   156
27764
e0ee3cc240fe advance: single argument (again);
wenzelm
parents: 27759
diff changeset
   157
fun range pos pos' = (encode_range (pos, pos'), pos');
27741
d2523b72ed44 added report;
wenzelm
parents: 27736
diff changeset
   158
27764
e0ee3cc240fe advance: single argument (again);
wenzelm
parents: 27759
diff changeset
   159
e0ee3cc240fe advance: single argument (again);
wenzelm
parents: 27759
diff changeset
   160
(* thread data *)
e0ee3cc240fe advance: single argument (again);
wenzelm
parents: 27759
diff changeset
   161
e0ee3cc240fe advance: single argument (again);
wenzelm
parents: 27759
diff changeset
   162
local val tag = Universal.tag () : T Universal.tag in
27741
d2523b72ed44 added report;
wenzelm
parents: 27736
diff changeset
   163
28122
3d099ce624e7 Thread.getLocal/setLocal;
wenzelm
parents: 28017
diff changeset
   164
fun thread_data () = the_default none (Thread.getLocal tag);
27764
e0ee3cc240fe advance: single argument (again);
wenzelm
parents: 27759
diff changeset
   165
e0ee3cc240fe advance: single argument (again);
wenzelm
parents: 27759
diff changeset
   166
fun setmp_thread_data pos f x =
e0ee3cc240fe advance: single argument (again);
wenzelm
parents: 27759
diff changeset
   167
  if ! Output.debugging then f x
e0ee3cc240fe advance: single argument (again);
wenzelm
parents: 27759
diff changeset
   168
  else Library.setmp_thread_data tag (thread_data ()) pos f x;
e0ee3cc240fe advance: single argument (again);
wenzelm
parents: 27759
diff changeset
   169
e0ee3cc240fe advance: single argument (again);
wenzelm
parents: 27759
diff changeset
   170
fun setmp_thread_data_seq pos f x =
e0ee3cc240fe advance: single argument (again);
wenzelm
parents: 27759
diff changeset
   171
  setmp_thread_data pos f x |> Seq.wrap (fn pull => setmp_thread_data pos pull ());
27741
d2523b72ed44 added report;
wenzelm
parents: 27736
diff changeset
   172
5010
9101b70b696d moved Thy/position.ML to General/position.ML;
wenzelm
parents:
diff changeset
   173
end;
27764
e0ee3cc240fe advance: single argument (again);
wenzelm
parents: 27759
diff changeset
   174
e0ee3cc240fe advance: single argument (again);
wenzelm
parents: 27759
diff changeset
   175
end;