author | wenzelm |
Fri, 15 Aug 2008 22:16:14 +0200 | |
changeset 27905 | 070b4a6a9d58 |
parent 27864 | 827730aea9e8 |
child 27984 | b4dd58cff97c |
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 |
|
27797 | 19 |
val content: T list -> string |
27852 | 20 |
val untabify_content: T list -> string |
27763 | 21 |
val is_eof: T -> bool |
22 |
val stopper: T Scan.stopper |
|
23 |
val !!! : string -> (T list -> 'a) -> T list -> 'a |
|
27778
3ec7a4d9ef18
renamed SymbolPos.scan_position to SymbolPos.scan_pos;
wenzelm
parents:
27763
diff
changeset
|
24 |
val scan_pos: T list -> Position.T * T list |
27763 | 25 |
val scan_comment: (string -> (T list -> T list * T list) -> T list -> T list * T list) -> |
26 |
T list -> T list * T list |
|
27 |
val scan_comment_body: (string -> (T list -> T list * T list) -> T list -> T list * T list) -> |
|
28 |
T list -> T list * T list |
|
29 |
val source: Position.T -> (Symbol.symbol, 'a) Source.source -> |
|
30 |
(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
|
31 |
type text = string |
27797 | 32 |
val implode: T list -> text |
33 |
val range: T list -> Position.range |
|
34 |
val implode_range: Position.T -> Position.T -> T list -> text * Position.range |
|
27778
3ec7a4d9ef18
renamed SymbolPos.scan_position to SymbolPos.scan_pos;
wenzelm
parents:
27763
diff
changeset
|
35 |
val explode: text * Position.T -> T list |
27763 | 36 |
end; |
37 |
||
38 |
structure SymbolPos: SYMBOL_POS = |
|
39 |
struct |
|
40 |
||
41 |
(* type T *) |
|
42 |
||
43 |
type T = Symbol.symbol * Position.T; |
|
44 |
||
45 |
fun symbol ((s, _): T) = s; |
|
27852 | 46 |
|
47 |
||
48 |
(* content *) |
|
49 |
||
27797 | 50 |
val content = implode o map symbol; |
27763 | 51 |
|
52 |
||
27864 | 53 |
val tab_width = (8: int); |
27852 | 54 |
|
55 |
fun untabify ("\t", pos) = |
|
56 |
(case Position.column_of pos of |
|
57 |
SOME n => Symbol.spaces (tab_width - ((n - 1) mod tab_width)) |
|
58 |
| NONE => error "No column information -- cannot interpret tabulators") |
|
59 |
| untabify (s, _) = s; |
|
60 |
||
61 |
val untabify_content = implode o map untabify; |
|
62 |
||
63 |
||
27763 | 64 |
(* stopper *) |
65 |
||
66 |
fun mk_eof pos = (Symbol.eof, pos); |
|
67 |
val eof = mk_eof Position.none; |
|
68 |
||
69 |
val is_eof = Symbol.is_eof o symbol; |
|
70 |
||
71 |
val stopper = |
|
72 |
Scan.stopper (fn [] => eof | inp => mk_eof (List.last inp |-> Position.advance)) is_eof; |
|
73 |
||
74 |
||
75 |
(* basic scanners *) |
|
76 |
||
77 |
fun !!! text scan = |
|
78 |
let |
|
79 |
fun get_pos [] = " (past end-of-text!)" |
|
80 |
| get_pos ((_, pos) :: _) = Position.str_of pos; |
|
81 |
||
82 |
fun err (syms, msg) = |
|
83 |
text ^ get_pos syms ^ " at " ^ Symbol.beginning 10 (map symbol syms) ^ |
|
84 |
(case msg of NONE => "" | SOME s => "\n" ^ s); |
|
85 |
in Scan.!! err scan end; |
|
86 |
||
87 |
fun $$$ s = Scan.one (fn x => symbol x = s) >> single; |
|
88 |
fun ~$$$ s = Scan.one (fn x => symbol x <> s) >> single; |
|
89 |
||
27778
3ec7a4d9ef18
renamed SymbolPos.scan_position to SymbolPos.scan_pos;
wenzelm
parents:
27763
diff
changeset
|
90 |
val scan_pos = Scan.ahead (Scan.one (K true)) >> (fn (_, pos): T => pos); |
27763 | 91 |
|
92 |
||
93 |
(* ML-style comments *) |
|
94 |
||
95 |
local |
|
96 |
||
97 |
val scan_cmt = |
|
98 |
Scan.depend (fn (d: int) => $$$ "(" @@@ $$$ "*" >> pair (d + 1)) || |
|
99 |
Scan.depend (fn 0 => Scan.fail | d => $$$ "*" @@@ $$$ ")" >> pair (d - 1)) || |
|
100 |
Scan.lift ($$$ "*" --| Scan.ahead (~$$$ ")")) || |
|
101 |
Scan.lift (Scan.one (fn (s, _) => s <> "*" andalso Symbol.is_regular s)) >> single; |
|
102 |
||
103 |
val scan_body = Scan.pass 0 (Scan.repeat scan_cmt >> flat); |
|
104 |
||
105 |
in |
|
106 |
||
107 |
fun scan_comment cut = |
|
108 |
$$$ "(" @@@ $$$ "*" @@@ cut "missing end of comment" (scan_body @@@ $$$ "*" @@@ $$$ ")"); |
|
109 |
||
110 |
fun scan_comment_body cut = |
|
111 |
$$$ "(" |-- $$$ "*" |-- cut "missing end of comment" (scan_body --| $$$ "*" --| $$$ ")"); |
|
112 |
||
113 |
end; |
|
114 |
||
115 |
||
116 |
(* source *) |
|
117 |
||
118 |
fun source pos = |
|
119 |
Source.source' pos Symbol.stopper (Scan.bulk (Scan.depend (fn pos => |
|
120 |
Scan.one Symbol.not_eof >> (fn s => (Position.advance s pos, (s, pos)))))) NONE; |
|
121 |
||
122 |
||
123 |
(* compact representation -- with Symbol.DEL padding *) |
|
124 |
||
27778
3ec7a4d9ef18
renamed SymbolPos.scan_position to SymbolPos.scan_pos;
wenzelm
parents:
27763
diff
changeset
|
125 |
type text = string; |
3ec7a4d9ef18
renamed SymbolPos.scan_position to SymbolPos.scan_pos;
wenzelm
parents:
27763
diff
changeset
|
126 |
|
27763 | 127 |
fun pad [] = [] |
128 |
| pad [(s, _)] = [s] |
|
129 |
| pad ((s1, pos1) :: (rest as (s2, pos2) :: _)) = |
|
130 |
let |
|
131 |
val end_pos1 = Position.advance s1 pos1; |
|
27797 | 132 |
val d = Int.max (0, Position.distance_of end_pos1 pos2); |
27763 | 133 |
in s1 :: replicate d Symbol.DEL @ pad rest end; |
134 |
||
27797 | 135 |
val implode = implode o pad; |
27763 | 136 |
|
27797 | 137 |
fun range (syms as (_, pos) :: _) = |
27763 | 138 |
let val pos' = List.last syms |-> Position.advance |
27797 | 139 |
in Position.range pos pos' end |
140 |
| range [] = Position.no_range; |
|
27763 | 141 |
|
27797 | 142 |
fun implode_range pos1 pos2 syms = |
143 |
let val syms' = (("", pos1) :: syms @ [("", pos2)]) |
|
144 |
in (implode syms', range syms') end; |
|
27778
3ec7a4d9ef18
renamed SymbolPos.scan_position to SymbolPos.scan_pos;
wenzelm
parents:
27763
diff
changeset
|
145 |
|
27763 | 146 |
fun explode (str, pos) = |
27778
3ec7a4d9ef18
renamed SymbolPos.scan_position to SymbolPos.scan_pos;
wenzelm
parents:
27763
diff
changeset
|
147 |
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
|
148 |
(Symbol.explode str) (Position.reset_range pos) |
27763 | 149 |
|> #1 |> filter_out (fn (s, _) => s = Symbol.DEL); |
150 |
||
151 |
end; |
|
152 |
||
153 |
structure BasicSymbolPos: BASIC_SYMBOL_POS = SymbolPos; (*not open by default*) |
|
154 |