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