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