author | wenzelm |
Tue, 05 Aug 2008 13:31:38 +0200 | |
changeset 27741 | d2523b72ed44 |
parent 27736 | 3703dbd0cdea |
child 27744 | d4c5ddf98869 |
permissions | -rw-r--r-- |
6118 | 1 |
(* Title: Pure/General/position.ML |
5010 | 2 |
ID: $Id$ |
3 |
Author: Markus Wenzel, TU Muenchen |
|
4 |
||
23673 | 5 |
Source positions. |
5010 | 6 |
*) |
7 |
||
8 |
signature POSITION = |
|
9 |
sig |
|
10 |
type T |
|
23673 | 11 |
val line_of: T -> int option |
26003 | 12 |
val column_of: T -> int option |
23673 | 13 |
val file_of: T -> string option |
5010 | 14 |
val none: T |
26882 | 15 |
val line_file: int -> string -> T |
5010 | 16 |
val line: int -> T |
23673 | 17 |
val file: string -> T |
26003 | 18 |
val advance: Symbol.symbol -> T -> T |
27426 | 19 |
val get_id: T -> string option |
20 |
val put_id: string -> T -> T |
|
25817 | 21 |
val of_properties: Markup.property list -> T |
23627 | 22 |
val properties_of: T -> Markup.property list |
26052 | 23 |
val default_properties: T -> Markup.property list -> Markup.property list |
26003 | 24 |
val str_of: T -> string |
25817 | 25 |
val thread_data: unit -> T |
26 |
val setmp_thread_data: T -> ('a -> 'b) -> 'a -> 'b |
|
25954 | 27 |
val setmp_thread_data_seq: T -> ('a -> 'b Seq.seq) -> 'a -> 'b Seq.seq |
27736 | 28 |
type range = T * T |
29 |
val encode_range: range -> T |
|
27741 | 30 |
val report: Markup.T -> T -> unit |
5010 | 31 |
end; |
32 |
||
33 |
structure Position: POSITION = |
|
34 |
struct |
|
35 |
||
36 |
(* datatype position *) |
|
37 |
||
26003 | 38 |
datatype T = Pos of (int * int) option * Markup.property list; |
39 |
||
40 |
fun line_of (Pos (SOME (m, _), _)) = SOME m |
|
41 |
| line_of _ = NONE; |
|
5010 | 42 |
|
26003 | 43 |
fun column_of (Pos (SOME (_, n), _)) = SOME n |
44 |
| column_of _ = NONE; |
|
5010 | 45 |
|
26003 | 46 |
fun file_of (Pos (_, props)) = AList.lookup (op =) props Markup.fileN; |
5010 | 47 |
|
26882 | 48 |
|
25817 | 49 |
val none = Pos (NONE, []); |
26882 | 50 |
|
51 |
fun line_file m name = Pos (SOME (m, 1), if name = "" then [] else [(Markup.fileN, name)]); |
|
52 |
fun line m = line_file m ""; |
|
53 |
val file = line_file 1; |
|
54 |
||
5010 | 55 |
|
26003 | 56 |
fun advance "\n" (Pos (SOME (m, _), props)) = Pos (SOME (m + 1, 1), props) |
26633
ff317b19e24e
advance: do not count utf8 trailer bytes (which happen to be undefined or punctuation in iso-latin);
wenzelm
parents:
26052
diff
changeset
|
57 |
| advance s (pos as Pos (SOME (m, n), props)) = |
ff317b19e24e
advance: do not count utf8 trailer bytes (which happen to be undefined or punctuation in iso-latin);
wenzelm
parents:
26052
diff
changeset
|
58 |
if Symbol.is_regular s andalso not (Symbol.is_utf8_trailer s) |
ff317b19e24e
advance: do not count utf8 trailer bytes (which happen to be undefined or punctuation in iso-latin);
wenzelm
parents:
26052
diff
changeset
|
59 |
then Pos (SOME (m, n + 1), props) else pos |
26003 | 60 |
| advance _ pos = pos; |
5010 | 61 |
|
23627 | 62 |
|
63 |
(* markup properties *) |
|
22158 | 64 |
|
27426 | 65 |
fun get_id (Pos (_, props)) = AList.lookup (op =) props Markup.idN; |
66 |
fun put_id id (Pos (count, props)) = Pos (count, AList.update (op =) (Markup.idN, id) props); |
|
67 |
||
26003 | 68 |
fun get_int props (name: string) = |
69 |
(case AList.lookup (op =) props name of |
|
70 |
NONE => NONE |
|
71 |
| SOME s => Int.fromString s); |
|
72 |
||
25817 | 73 |
fun of_properties props = |
23627 | 74 |
let |
26003 | 75 |
val count = |
76 |
(case get_int props Markup.lineN of |
|
77 |
NONE => NONE |
|
78 |
| SOME m => SOME (m, the_default 1 (get_int props Markup.columnN))); |
|
79 |
fun property name = the_list (find_first (fn (x: string, _) => x = name) props); |
|
80 |
in (Pos (count, property Markup.fileN @ property Markup.idN)) end; |
|
81 |
||
82 |
fun properties_of (Pos (count, props)) = |
|
83 |
(case count of |
|
84 |
NONE => [] |
|
85 |
| SOME (m, n) => [(Markup.lineN, string_of_int m), (Markup.columnN, string_of_int n)]) @ props; |
|
86 |
||
26052 | 87 |
fun default_properties default props = |
88 |
if exists (member (op =) Markup.position_properties o #1) props then props |
|
89 |
else properties_of default @ props; |
|
90 |
||
25817 | 91 |
|
26003 | 92 |
(* str_of *) |
93 |
||
94 |
fun str_of pos = |
|
95 |
let |
|
96 |
val props = properties_of pos; |
|
97 |
val s = |
|
98 |
(case (line_of pos, file_of pos) of |
|
99 |
(SOME m, NONE) => "(line " ^ string_of_int m ^ ")" |
|
100 |
| (SOME m, SOME name) => "(line " ^ string_of_int m ^ " of " ^ quote name ^ ")" |
|
101 |
| _ => ""); |
|
102 |
in |
|
103 |
if null props then "" |
|
104 |
else (if s = "" then "" else " ") ^ Markup.markup (Markup.properties props Markup.position) s |
|
105 |
end; |
|
25817 | 106 |
|
23627 | 107 |
|
25817 | 108 |
(* thread data *) |
109 |
||
110 |
local val tag = Universal.tag () : T Universal.tag in |
|
111 |
||
112 |
fun thread_data () = the_default none (Multithreading.get_data tag); |
|
26890
f9ec18f7c0f6
setmp_thread_data: do nothing if Output.debugging;
wenzelm
parents:
26882
diff
changeset
|
113 |
|
f9ec18f7c0f6
setmp_thread_data: do nothing if Output.debugging;
wenzelm
parents:
26882
diff
changeset
|
114 |
fun setmp_thread_data pos f x = |
f9ec18f7c0f6
setmp_thread_data: do nothing if Output.debugging;
wenzelm
parents:
26882
diff
changeset
|
115 |
if ! Output.debugging then f x |
f9ec18f7c0f6
setmp_thread_data: do nothing if Output.debugging;
wenzelm
parents:
26882
diff
changeset
|
116 |
else Library.setmp_thread_data tag (thread_data ()) pos f x; |
25817 | 117 |
|
25954 | 118 |
fun setmp_thread_data_seq pos f seq = |
119 |
setmp_thread_data pos f seq |> Seq.wrap (fn pull => setmp_thread_data pos pull ()); |
|
120 |
||
25817 | 121 |
end; |
23673 | 122 |
|
27736 | 123 |
|
124 |
(* range *) |
|
125 |
||
126 |
type range = T * T; |
|
127 |
||
128 |
fun encode_range (Pos (count, props), Pos (end_count, _)) = |
|
129 |
let val props' = props |> fold_rev (AList.update op =) |
|
130 |
(case end_count of |
|
131 |
NONE => [] |
|
132 |
| SOME (m, n) => [(Markup.end_lineN, string_of_int m), (Markup.end_columnN, string_of_int n)]) |
|
133 |
in Pos (count, props') end; |
|
134 |
||
27741 | 135 |
|
136 |
(* report markup *) |
|
137 |
||
138 |
fun report markup pos = |
|
139 |
if pos = none then () |
|
140 |
else Output.status (Markup.markup (Markup.properties (properties_of pos) markup) ""); |
|
141 |
||
5010 | 142 |
end; |