src/Pure/General/position.ML
author wenzelm
Wed Apr 06 16:33:33 2016 +0200 (2016-04-06)
changeset 62889 99c7f31615c2
parent 62803 5f73bf6ba98b
child 62929 b92565f98206
permissions -rw-r--r--
clarified modules;
tuned signature;
     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 advance_offset: int -> T -> T
    18   val distance_of: T -> T -> int
    19   val none: T
    20   val start: T
    21   val file_name: string -> Properties.T
    22   val file_only: string -> T
    23   val file: string -> T
    24   val line_file_only: int -> string -> T
    25   val line_file: int -> string -> T
    26   val line: int -> T
    27   val id: string -> T
    28   val id_only: string -> T
    29   val get_id: T -> string option
    30   val put_id: string -> T -> T
    31   val parse_id: T -> int option
    32   val of_properties: Properties.T -> T
    33   val properties_of: T -> Properties.T
    34   val def_properties_of: T -> Properties.T
    35   val entity_properties_of: bool -> serial -> T -> Properties.T
    36   val default_properties: T -> Properties.T -> Properties.T
    37   val markup: T -> Markup.T -> Markup.T
    38   val is_reported: T -> bool
    39   val is_reported_range: T -> bool
    40   val reported_text: T -> Markup.T -> string -> string
    41   val report_text: T -> Markup.T -> string -> unit
    42   val report: T -> Markup.T -> unit
    43   type report = T * Markup.T
    44   type report_text = report * string
    45   val reports_text: report_text list -> unit
    46   val reports: report list -> unit
    47   val store_reports: report_text list Unsynchronized.ref ->
    48     T list -> ('a -> Markup.T list) -> 'a -> unit
    49   val append_reports: report_text list Unsynchronized.ref -> report list -> unit
    50   val here: T -> string
    51   val here_list: T list -> string
    52   type range = T * T
    53   val no_range: range
    54   val no_range_position: T -> T
    55   val range_position: range -> T
    56   val range: T * T -> range
    57   val range_of_properties: Properties.T -> range
    58   val properties_of_range: range -> Properties.T
    59   val thread_data: unit -> T
    60   val setmp_thread_data: T -> ('a -> 'b) -> 'a -> 'b
    61   val default: T -> bool * T
    62 end;
    63 
    64 structure Position: POSITION =
    65 struct
    66 
    67 (* datatype position *)
    68 
    69 datatype T = Pos of (int * int * int) * Properties.T;
    70 
    71 fun norm_props (props: Properties.T) =
    72   maps (fn a => the_list (find_first (fn (b, _) => a = b) props))
    73     Markup.position_properties';
    74 
    75 fun make {line = i, offset = j, end_offset = k, props} = Pos ((i, j, k), norm_props props);
    76 fun dest (Pos ((i, j, k), props)) = {line = i, offset = j, end_offset = k, props = props};
    77 
    78 fun valid (i: int) = i > 0;
    79 fun if_valid i i' = if valid i then i' else i;
    80 
    81 
    82 (* fields *)
    83 
    84 fun line_of (Pos ((i, _, _), _)) = if valid i then SOME i else NONE;
    85 fun offset_of (Pos ((_, j, _), _)) = if valid j then SOME j else NONE;
    86 fun end_offset_of (Pos ((_, _, k), _)) = if valid k then SOME k else NONE;
    87 
    88 fun file_of (Pos (_, props)) = Properties.get props Markup.fileN;
    89 
    90 
    91 (* advance *)
    92 
    93 fun advance_count "\n" (i: int, j: int, k: int) =
    94       (if_valid i (i + 1), if_valid j (j + 1), k)
    95   | advance_count s (i, j, k) =
    96       if Symbol.not_eof s then (i, if_valid j (j + 1), k)
    97       else (i, j, k);
    98 
    99 fun invalid_count (i, j, _: int) =
   100   not (valid i orelse valid j);
   101 
   102 fun advance sym (pos as (Pos (count, props))) =
   103   if invalid_count count then pos else Pos (advance_count sym count, props);
   104 
   105 fun advance_offset offset (pos as (Pos (count as (i, j, k), props))) =
   106   if invalid_count count then pos
   107   else if valid i then raise Fail "Illegal line position"
   108   else Pos ((i, if_valid j (j + offset), k), props);
   109 
   110 
   111 (* distance of adjacent positions *)
   112 
   113 fun distance_of (Pos ((_, j, _), _)) (Pos ((_, j', _), _)) =
   114   if valid j andalso valid j' then j' - j
   115   else 0;
   116 
   117 
   118 (* make position *)
   119 
   120 val none = Pos ((0, 0, 0), []);
   121 val start = Pos ((1, 1, 0), []);
   122 
   123 
   124 fun file_name "" = []
   125   | file_name name = [(Markup.fileN, name)];
   126 
   127 fun file_only name = Pos ((0, 0, 0), file_name name);
   128 fun file name = Pos ((1, 1, 0), file_name name);
   129 
   130 fun line_file_only i name = Pos ((i, 0, 0), file_name name);
   131 fun line_file i name = Pos ((i, 1, 0), file_name name);
   132 fun line i = line_file i "";
   133 
   134 fun id id = Pos ((0, 1, 0), [(Markup.idN, id)]);
   135 fun id_only id = Pos ((0, 0, 0), [(Markup.idN, id)]);
   136 
   137 fun get_id (Pos (_, props)) = Properties.get props Markup.idN;
   138 fun put_id id (Pos (count, props)) = Pos (count, norm_props (Properties.put (Markup.idN, id) props));
   139 
   140 fun parse_id pos = Option.map Markup.parse_int (get_id pos);
   141 
   142 
   143 (* markup properties *)
   144 
   145 fun get props name =
   146   (case Properties.get props name of
   147     NONE => 0
   148   | SOME s => Markup.parse_int s);
   149 
   150 fun of_properties props =
   151   make {line = get props Markup.lineN,
   152     offset = get props Markup.offsetN,
   153     end_offset = get props Markup.end_offsetN,
   154     props = props};
   155 
   156 fun value k i = if valid i then [(k, Markup.print_int i)] else [];
   157 
   158 fun properties_of (Pos ((i, j, k), props)) =
   159   value Markup.lineN i @ value Markup.offsetN j @ value Markup.end_offsetN k @ props;
   160 
   161 val def_properties_of = properties_of #> map (fn (x, y) => ("def_" ^ x, y));
   162 
   163 fun entity_properties_of def serial pos =
   164   if def then (Markup.defN, Markup.print_int serial) :: properties_of pos
   165   else (Markup.refN, Markup.print_int serial) :: def_properties_of pos;
   166 
   167 fun default_properties default props =
   168   if exists (member (op =) Markup.position_properties o #1) props then props
   169   else properties_of default @ props;
   170 
   171 val markup = Markup.properties o properties_of;
   172 
   173 
   174 (* reports *)
   175 
   176 fun is_reported pos = is_some (offset_of pos) andalso is_some (get_id pos);
   177 fun is_reported_range pos = is_reported pos andalso is_some (end_offset_of pos);
   178 
   179 fun reported_text pos m txt = if is_reported pos then Markup.markup (markup pos m) txt else "";
   180 fun report_text pos markup txt = Output.report [reported_text pos markup txt];
   181 fun report pos markup = report_text pos markup "";
   182 
   183 type report = T * Markup.T;
   184 type report_text = report * string;
   185 
   186 val reports_text =
   187   map (fn ((pos, m), txt) => if is_reported pos then Markup.markup (markup pos m) txt else "")
   188   #> Output.report;
   189 
   190 val reports = map (rpair "") #> reports_text;
   191 
   192 fun store_reports _ [] _ _ = ()
   193   | store_reports (r: report_text list Unsynchronized.ref) ps markup x =
   194       let val ms = markup x
   195       in Unsynchronized.change r (fold (fn p => fold (fn m => cons ((p, m), "")) ms) ps) end;
   196 
   197 fun append_reports (r: report_text list Unsynchronized.ref) reports =
   198   Unsynchronized.change r (append (map (rpair "") reports));
   199 
   200 
   201 (* here: user output *)
   202 
   203 fun here pos =
   204   let
   205     val props = properties_of pos;
   206     val (s1, s2) =
   207       (case (line_of pos, file_of pos) of
   208         (SOME i, NONE) => (" ", "(line " ^ Markup.print_int i ^ ")")
   209       | (SOME i, SOME name) => (" ", "(line " ^ Markup.print_int i ^ " of " ^ quote name ^ ")")
   210       | (NONE, SOME name) => (" ", "(file " ^ quote name ^ ")")
   211       | _ => if is_reported pos then ("", "\<here>") else ("", ""));
   212   in
   213     if null props then ""
   214     else s1 ^ Markup.markup (Markup.properties props Markup.position) s2
   215   end;
   216 
   217 val here_list = implode o map here;
   218 
   219 
   220 (* range *)
   221 
   222 type range = T * T;
   223 
   224 val no_range = (none, none);
   225 
   226 fun no_range_position (Pos ((i, j, _), props)) = Pos ((i, j, 0), props);
   227 fun range_position (Pos ((i, j, _), props), Pos ((_, j', _), _)) = Pos ((i, j, j'), props);
   228 fun range (pos, pos') = (range_position (pos, pos'), no_range_position pos');
   229 
   230 fun range_of_properties props =
   231   let
   232     val pos = of_properties props;
   233     val pos' =
   234       make {line = get props Markup.end_lineN,
   235         offset = get props Markup.end_offsetN,
   236         end_offset = 0,
   237         props = props};
   238   in (pos, pos') end;
   239 
   240 fun properties_of_range (pos, pos') =
   241   properties_of pos @ value Markup.end_lineN (the_default 0 (line_of pos'));
   242 
   243 
   244 (* thread data *)
   245 
   246 val thread_data_var = Thread_Data.var () : T Thread_Data.var;
   247 fun thread_data () = the_default none (Thread_Data.get thread_data_var);
   248 fun setmp_thread_data pos = Thread_Data.setmp thread_data_var (SOME pos);
   249 
   250 fun default pos =
   251   if pos = none then (false, thread_data ())
   252   else (true, pos);
   253 
   254 end;