author | wenzelm |
Thu, 07 Aug 2008 19:21:40 +0200 | |
changeset 27778 | 3ec7a4d9ef18 |
parent 27763 | f49f6275cefa |
child 27797 | 9861b39a2fd5 |
permissions | -rw-r--r-- |
27763 | 1 |
(* Title: Pure/General/symbol_pos.ML |
2 |
ID: $Id$ |
|
3 |
Author: Makarius |
|
4 |
||
5 |
Symbols with explicit position information. |
|
6 |
*) |
|
7 |
||
8 |
signature BASIC_SYMBOL_POS = |
|
9 |
sig |
|
10 |
type T = Symbol.symbol * Position.T |
|
11 |
val symbol: T -> Symbol.symbol |
|
12 |
val $$$ : Symbol.symbol -> T list -> T list * T list |
|
13 |
val ~$$$ : Symbol.symbol -> T list -> T list * T list |
|
14 |
end |
|
15 |
||
16 |
signature SYMBOL_POS = |
|
17 |
sig |
|
18 |
include BASIC_SYMBOL_POS |
|
19 |
val is_eof: T -> bool |
|
20 |
val stopper: T Scan.stopper |
|
21 |
val !!! : string -> (T list -> 'a) -> T list -> 'a |
|
27778
3ec7a4d9ef18
renamed SymbolPos.scan_position to SymbolPos.scan_pos;
wenzelm
parents:
27763
diff
changeset
|
22 |
val scan_pos: T list -> Position.T * T list |
27763 | 23 |
val scan_comment: (string -> (T list -> T list * T list) -> T list -> T list * T list) -> |
24 |
T list -> T list * T list |
|
25 |
val scan_comment_body: (string -> (T list -> T list * T list) -> T list -> T list * T list) -> |
|
26 |
T list -> T list * T list |
|
27 |
val source: Position.T -> (Symbol.symbol, 'a) Source.source -> |
|
28 |
(T, Position.T * (Symbol.symbol, 'a) Source.source) Source.source |
|
27778
3ec7a4d9ef18
renamed SymbolPos.scan_position to SymbolPos.scan_pos;
wenzelm
parents:
27763
diff
changeset
|
29 |
type text = string |
3ec7a4d9ef18
renamed SymbolPos.scan_position to SymbolPos.scan_pos;
wenzelm
parents:
27763
diff
changeset
|
30 |
val implode: T list -> text * Position.range |
3ec7a4d9ef18
renamed SymbolPos.scan_position to SymbolPos.scan_pos;
wenzelm
parents:
27763
diff
changeset
|
31 |
val implode_delim: Position.T -> Position.T -> T list -> text * Position.range |
3ec7a4d9ef18
renamed SymbolPos.scan_position to SymbolPos.scan_pos;
wenzelm
parents:
27763
diff
changeset
|
32 |
val explode: text * Position.T -> T list |
27763 | 33 |
end; |
34 |
||
35 |
structure SymbolPos: SYMBOL_POS = |
|
36 |
struct |
|
37 |
||
38 |
(* type T *) |
|
39 |
||
40 |
type T = Symbol.symbol * Position.T; |
|
41 |
||
42 |
fun symbol ((s, _): T) = s; |
|
43 |
||
44 |
||
45 |
(* stopper *) |
|
46 |
||
47 |
fun mk_eof pos = (Symbol.eof, pos); |
|
48 |
val eof = mk_eof Position.none; |
|
49 |
||
50 |
val is_eof = Symbol.is_eof o symbol; |
|
51 |
||
52 |
val stopper = |
|
53 |
Scan.stopper (fn [] => eof | inp => mk_eof (List.last inp |-> Position.advance)) is_eof; |
|
54 |
||
55 |
||
56 |
(* basic scanners *) |
|
57 |
||
58 |
fun !!! text scan = |
|
59 |
let |
|
60 |
fun get_pos [] = " (past end-of-text!)" |
|
61 |
| get_pos ((_, pos) :: _) = Position.str_of pos; |
|
62 |
||
63 |
fun err (syms, msg) = |
|
64 |
text ^ get_pos syms ^ " at " ^ Symbol.beginning 10 (map symbol syms) ^ |
|
65 |
(case msg of NONE => "" | SOME s => "\n" ^ s); |
|
66 |
in Scan.!! err scan end; |
|
67 |
||
68 |
fun $$$ s = Scan.one (fn x => symbol x = s) >> single; |
|
69 |
fun ~$$$ s = Scan.one (fn x => symbol x <> s) >> single; |
|
70 |
||
27778
3ec7a4d9ef18
renamed SymbolPos.scan_position to SymbolPos.scan_pos;
wenzelm
parents:
27763
diff
changeset
|
71 |
val scan_pos = Scan.ahead (Scan.one (K true)) >> (fn (_, pos): T => pos); |
27763 | 72 |
|
73 |
||
74 |
(* ML-style comments *) |
|
75 |
||
76 |
local |
|
77 |
||
78 |
val scan_cmt = |
|
79 |
Scan.depend (fn (d: int) => $$$ "(" @@@ $$$ "*" >> pair (d + 1)) || |
|
80 |
Scan.depend (fn 0 => Scan.fail | d => $$$ "*" @@@ $$$ ")" >> pair (d - 1)) || |
|
81 |
Scan.lift ($$$ "*" --| Scan.ahead (~$$$ ")")) || |
|
82 |
Scan.lift (Scan.one (fn (s, _) => s <> "*" andalso Symbol.is_regular s)) >> single; |
|
83 |
||
84 |
val scan_body = Scan.pass 0 (Scan.repeat scan_cmt >> flat); |
|
85 |
||
86 |
in |
|
87 |
||
88 |
fun scan_comment cut = |
|
89 |
$$$ "(" @@@ $$$ "*" @@@ cut "missing end of comment" (scan_body @@@ $$$ "*" @@@ $$$ ")"); |
|
90 |
||
91 |
fun scan_comment_body cut = |
|
92 |
$$$ "(" |-- $$$ "*" |-- cut "missing end of comment" (scan_body --| $$$ "*" --| $$$ ")"); |
|
93 |
||
94 |
end; |
|
95 |
||
96 |
||
97 |
(* source *) |
|
98 |
||
99 |
fun source pos = |
|
100 |
Source.source' pos Symbol.stopper (Scan.bulk (Scan.depend (fn pos => |
|
101 |
Scan.one Symbol.not_eof >> (fn s => (Position.advance s pos, (s, pos)))))) NONE; |
|
102 |
||
103 |
||
104 |
(* compact representation -- with Symbol.DEL padding *) |
|
105 |
||
27778
3ec7a4d9ef18
renamed SymbolPos.scan_position to SymbolPos.scan_pos;
wenzelm
parents:
27763
diff
changeset
|
106 |
type text = string; |
3ec7a4d9ef18
renamed SymbolPos.scan_position to SymbolPos.scan_pos;
wenzelm
parents:
27763
diff
changeset
|
107 |
|
27763 | 108 |
local |
109 |
||
110 |
fun pad [] = [] |
|
111 |
| pad [(s, _)] = [s] |
|
112 |
| pad ((s1, pos1) :: (rest as (s2, pos2) :: _)) = |
|
113 |
let |
|
114 |
fun err () = |
|
115 |
raise Fail ("Misaligned symbols: " ^ |
|
116 |
quote s1 ^ Position.str_of pos1 ^ " " ^ |
|
117 |
quote s2 ^ Position.str_of pos2); |
|
118 |
||
119 |
val end_pos1 = Position.advance s1 pos1; |
|
120 |
val _ = Position.line_of end_pos1 = Position.line_of pos2 orelse err (); |
|
121 |
val d = |
|
122 |
(case (Position.column_of end_pos1, Position.column_of pos2) of |
|
123 |
(NONE, NONE) => 0 |
|
124 |
| (SOME n1, SOME n2) => n2 - n1 |
|
125 |
| _ => err ()); |
|
126 |
val _ = d >= 0 orelse err (); |
|
127 |
in s1 :: replicate d Symbol.DEL @ pad rest end; |
|
128 |
||
129 |
val orig_implode = implode; |
|
130 |
||
131 |
in |
|
132 |
||
133 |
fun implode (syms as (_, pos) :: _) = |
|
134 |
let val pos' = List.last syms |-> Position.advance |
|
135 |
in (orig_implode (pad syms), Position.range pos pos') end |
|
136 |
| implode [] = ("", (Position.none, Position.none)); |
|
137 |
||
27778
3ec7a4d9ef18
renamed SymbolPos.scan_position to SymbolPos.scan_pos;
wenzelm
parents:
27763
diff
changeset
|
138 |
fun implode_delim pos1 pos2 syms = implode (("", pos1) :: syms @ [("", pos2)]); |
3ec7a4d9ef18
renamed SymbolPos.scan_position to SymbolPos.scan_pos;
wenzelm
parents:
27763
diff
changeset
|
139 |
|
27763 | 140 |
fun explode (str, pos) = |
27778
3ec7a4d9ef18
renamed SymbolPos.scan_position to SymbolPos.scan_pos;
wenzelm
parents:
27763
diff
changeset
|
141 |
fold_map (fn s => fn p => ((s, p), (Position.advance s p))) |
3ec7a4d9ef18
renamed SymbolPos.scan_position to SymbolPos.scan_pos;
wenzelm
parents:
27763
diff
changeset
|
142 |
(Symbol.explode str) (Position.reset_range pos) |
27763 | 143 |
|> #1 |> filter_out (fn (s, _) => s = Symbol.DEL); |
144 |
||
145 |
end; |
|
146 |
||
147 |
end; |
|
148 |
||
149 |
structure BasicSymbolPos: BASIC_SYMBOL_POS = SymbolPos; (*not open by default*) |
|
150 |