src/Pure/General/position.ML
author wenzelm
Tue Aug 16 21:54:06 2011 +0200 (2011-08-16)
changeset 44224 4040d0ffac7b
parent 44200 ce0112e26b3b
child 44735 66862d02678c
permissions -rw-r--r--
tuned message;
     1 (*  Title:      Pure/General/position.ML
     2     Author:     Markus Wenzel, TU Muenchen
     3 
     4 Source positions: counting Isabelle symbols, starting from 1.
     5 *)
     6 
     7 signature POSITION =
     8 sig
     9   eqtype T
    10   val make: {line: int, offset: int, end_offset: int, props: Properties.T} -> T
    11   val dest: T -> {line: int, offset: int, end_offset: int, props: Properties.T}
    12   val line_of: T -> int option
    13   val offset_of: T -> int option
    14   val end_offset_of: T -> int option
    15   val file_of: T -> string option
    16   val advance: Symbol.symbol -> T -> T
    17   val distance_of: T -> T -> int
    18   val none: T
    19   val start: T
    20   val file_name: string -> Properties.T
    21   val file_only: string -> T
    22   val file: string -> T
    23   val line: int -> T
    24   val line_file: int -> string -> T
    25   val id: string -> T
    26   val id_only: string -> T
    27   val get_id: T -> string option
    28   val put_id: string -> T -> T
    29   val of_properties: Properties.T -> T
    30   val properties_of: T -> Properties.T
    31   val def_properties_of: T -> Properties.T
    32   val default_properties: T -> Properties.T -> Properties.T
    33   val markup: T -> Markup.T -> Markup.T
    34   val is_reported: T -> bool
    35   val reported_text: T -> Markup.T -> string -> string
    36   val report_text: T -> Markup.T -> string -> unit
    37   val report: T -> Markup.T -> unit
    38   type reports = (T * Markup.T) list
    39   val reports: reports Unsynchronized.ref -> T list -> ('a -> Markup.T list) -> 'a -> unit
    40   val str_of: T -> string
    41   type range = T * T
    42   val no_range: range
    43   val set_range: range -> T
    44   val reset_range: T -> T
    45   val range: T -> T -> range
    46   val thread_data: unit -> T
    47   val setmp_thread_data: T -> ('a -> 'b) -> 'a -> 'b
    48   val default: T -> T
    49 end;
    50 
    51 structure Position: POSITION =
    52 struct
    53 
    54 (* datatype position *)
    55 
    56 datatype T = Pos of (int * int * int) * Properties.T;
    57 
    58 fun norm_props (props: Properties.T) =
    59   maps (fn a => the_list (find_first (fn (b, _) => a = b) props)) Markup.position_properties';
    60 
    61 fun make {line = i, offset = j, end_offset = k, props} = Pos ((i, j, k), norm_props props);
    62 fun dest (Pos ((i, j, k), props)) = {line = i, offset = j, end_offset = k, props = props};
    63 
    64 fun valid (i: int) = i > 0;
    65 fun if_valid i i' = if valid i then i' else i;
    66 
    67 
    68 (* fields *)
    69 
    70 fun line_of (Pos ((i, _, _), _)) = if valid i then SOME i else NONE;
    71 fun offset_of (Pos ((_, j, _), _)) = if valid j then SOME j else NONE;
    72 fun end_offset_of (Pos ((_, _, k), _)) = if valid k then SOME k else NONE;
    73 
    74 fun file_of (Pos (_, props)) = Properties.get props Markup.fileN;
    75 
    76 
    77 (* advance *)
    78 
    79 fun advance_count "\n" (i: int, j: int, k: int) =
    80       (if_valid i (i + 1), if_valid j (j + 1), k)
    81   | advance_count s (i, j, k) =
    82       if Symbol.is_regular s then (i, if_valid j (j + 1), k)
    83       else (i, j, k);
    84 
    85 fun invalid_count (i, j, _: int) =
    86   not (valid i orelse valid j);
    87 
    88 fun advance sym (pos as (Pos (count, props))) =
    89   if invalid_count count then pos else Pos (advance_count sym count, props);
    90 
    91 
    92 (* distance of adjacent positions *)
    93 
    94 fun distance_of (Pos ((_, j, _), _)) (Pos ((_, j', _), _)) =
    95   if valid j andalso valid j' then j' - j
    96   else 0;
    97 
    98 
    99 (* make position *)
   100 
   101 val none = Pos ((0, 0, 0), []);
   102 val start = Pos ((1, 1, 0), []);
   103 
   104 
   105 fun file_name "" = []
   106   | file_name name = [(Markup.fileN, name)];
   107 
   108 fun file_only name = Pos ((0, 0, 0), file_name name);
   109 fun file name = Pos ((1, 1, 0), file_name name);
   110 
   111 fun line_file i name = Pos ((i, 1, 0), file_name name);
   112 fun line i = line_file i "";
   113 
   114 fun id id = Pos ((0, 1, 0), [(Markup.idN, id)]);
   115 fun id_only id = Pos ((0, 0, 0), [(Markup.idN, id)]);
   116 
   117 fun get_id (Pos (_, props)) = Properties.get props Markup.idN;
   118 fun put_id id (Pos (count, props)) = Pos (count, Properties.put (Markup.idN, id) props);
   119 
   120 
   121 (* markup properties *)
   122 
   123 fun of_properties props =
   124   let
   125     fun get name =
   126       (case Properties.get props name of
   127         NONE => 0
   128       | SOME s => the_default 0 (Int.fromString s));
   129   in
   130     make {line = get Markup.lineN, offset = get Markup.offsetN,
   131       end_offset = get Markup.end_offsetN, props = props}
   132   end;
   133 
   134 
   135 fun value k i = if valid i then [(k, string_of_int i)] else [];
   136 
   137 fun properties_of (Pos ((i, j, k), props)) =
   138   value Markup.lineN i @ value Markup.offsetN j @ value Markup.end_offsetN k @ props;
   139 
   140 val def_properties_of = properties_of #> (map (fn (x, y) => ("def_" ^ x, y)));
   141 
   142 fun default_properties default props =
   143   if exists (member (op =) Markup.position_properties o #1) props then props
   144   else properties_of default @ props;
   145 
   146 val markup = Markup.properties o properties_of;
   147 
   148 
   149 (* reports *)
   150 
   151 fun is_reported pos = is_some (offset_of pos) andalso is_some (get_id pos);
   152 
   153 fun reported_text pos m txt = if is_reported pos then Markup.markup (markup pos m) txt else "";
   154 fun report_text pos markup txt = Output.report (reported_text pos markup txt);
   155 fun report pos markup = report_text pos markup "";
   156 
   157 type reports = (T * Markup.T) list;
   158 
   159 fun reports _ [] _ _ = ()
   160   | reports (r: reports Unsynchronized.ref) ps markup x =
   161       let val ms = markup x
   162       in Unsynchronized.change r (fold (fn p => fold (fn m => cons (p, m)) ms) ps) end;
   163 
   164 
   165 (* str_of *)
   166 
   167 fun str_of pos =
   168   let
   169     val props = properties_of pos;
   170     val s =
   171       (case (line_of pos, file_of pos) of
   172         (SOME i, NONE) => "(line " ^ string_of_int i ^ ")"
   173       | (SOME i, SOME name) => "(line " ^ string_of_int i ^ " of " ^ quote name ^ ")"
   174       | (NONE, SOME name) => "(file " ^ quote name ^ ")"
   175       | _ => "");
   176   in
   177     if null props then ""
   178     else (if s = "" then "" else " ") ^ Markup.markup (Markup.properties props Markup.position) s
   179   end;
   180 
   181 
   182 (* range *)
   183 
   184 type range = T * T;
   185 
   186 val no_range = (none, none);
   187 
   188 fun set_range (Pos ((i, j, _), props), Pos ((_, j', _), _)) = Pos ((i, j, j'), props);
   189 fun reset_range (Pos ((i, j, _), props)) = Pos ((i, j, 0), props);
   190 
   191 fun range pos pos' = (set_range (pos, pos'), pos');
   192 
   193 
   194 (* thread data *)
   195 
   196 local val tag = Universal.tag () : T Universal.tag in
   197 
   198 fun thread_data () = the_default none (Thread.getLocal tag);
   199 
   200 fun setmp_thread_data pos = Library.setmp_thread_data tag (thread_data ()) pos;
   201 
   202 end;
   203 
   204 fun default pos =
   205   if pos = none then thread_data ()
   206   else pos;
   207 
   208 end;