1 (* Title: Pure/General/symbol_pos.ML
5 Symbols with explicit position information.
8 signature BASIC_SYMBOL_POS =
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
16 signature SYMBOL_POS =
18 include BASIC_SYMBOL_POS
20 val stopper: T Scan.stopper
21 val !!! : string -> (T list -> 'a) -> T list -> 'a
22 val scan_pos: T list -> Position.T * T list
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
30 val implode: T list -> text * Position.range
31 val implode_delim: Position.T -> Position.T -> T list -> text * Position.range
32 val explode: text * Position.T -> T list
35 structure SymbolPos: SYMBOL_POS =
40 type T = Symbol.symbol * Position.T;
42 fun symbol ((s, _): T) = s;
47 fun mk_eof pos = (Symbol.eof, pos);
48 val eof = mk_eof Position.none;
50 val is_eof = Symbol.is_eof o symbol;
53 Scan.stopper (fn [] => eof | inp => mk_eof (List.last inp |-> Position.advance)) is_eof;
60 fun get_pos [] = " (past end-of-text!)"
61 | get_pos ((_, pos) :: _) = Position.str_of pos;
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;
68 fun $$$ s = Scan.one (fn x => symbol x = s) >> single;
69 fun ~$$$ s = Scan.one (fn x => symbol x <> s) >> single;
71 val scan_pos = Scan.ahead (Scan.one (K true)) >> (fn (_, pos): T => pos);
74 (* ML-style comments *)
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;
84 val scan_body = Scan.pass 0 (Scan.repeat scan_cmt >> flat);
88 fun scan_comment cut =
89 $$$ "(" @@@ $$$ "*" @@@ cut "missing end of comment" (scan_body @@@ $$$ "*" @@@ $$$ ")");
91 fun scan_comment_body cut =
92 $$$ "(" |-- $$$ "*" |-- cut "missing end of comment" (scan_body --| $$$ "*" --| $$$ ")");
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;
104 (* compact representation -- with Symbol.DEL padding *)
112 | pad ((s1, pos1) :: (rest as (s2, pos2) :: _)) =
115 raise Fail ("Misaligned symbols: " ^
116 quote s1 ^ Position.str_of pos1 ^ " " ^
117 quote s2 ^ Position.str_of pos2);
119 val end_pos1 = Position.advance s1 pos1;
120 val _ = Position.line_of end_pos1 = Position.line_of pos2 orelse err ();
122 (case (Position.column_of end_pos1, Position.column_of pos2) of
124 | (SOME n1, SOME n2) => n2 - n1
126 val _ = d >= 0 orelse err ();
127 in s1 :: replicate d Symbol.DEL @ pad rest end;
129 val orig_implode = implode;
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));
138 fun implode_delim pos1 pos2 syms = implode (("", pos1) :: syms @ [("", pos2)]);
140 fun explode (str, pos) =
141 fold_map (fn s => fn p => ((s, p), (Position.advance s p)))
142 (Symbol.explode str) (Position.reset_range pos)
143 |> #1 |> filter_out (fn (s, _) => s = Symbol.DEL);
149 structure BasicSymbolPos: BASIC_SYMBOL_POS = SymbolPos; (*not open by default*)