8 sig |
8 sig |
9 datatype kind = Command_Span of string * Position.T | Ignored_Span | Malformed_Span |
9 datatype kind = Command_Span of string * Position.T | Ignored_Span | Malformed_Span |
10 datatype span = Span of kind * Token.T list |
10 datatype span = Span of kind * Token.T list |
11 val kind: span -> kind |
11 val kind: span -> kind |
12 val content: span -> Token.T list |
12 val content: span -> Token.T list |
13 val position: span -> Position.T |
13 val symbol_length: span -> int option |
14 val symbol_length: span -> int |
14 val adjust_offsets_kind: (int -> int option) -> kind -> kind |
|
15 val adjust_offsets: (int -> int option) -> span -> span |
15 end; |
16 end; |
16 |
17 |
17 structure Command_Span: COMMAND_SPAN = |
18 structure Command_Span: COMMAND_SPAN = |
18 struct |
19 struct |
19 |
20 |
20 datatype kind = Command_Span of string * Position.T | Ignored_Span | Malformed_Span; |
21 datatype kind = Command_Span of string * Position.T | Ignored_Span | Malformed_Span; |
21 datatype span = Span of kind * Token.T list; |
22 datatype span = Span of kind * Token.T list; |
22 |
23 |
23 fun kind (Span (k, _)) = k; |
24 fun kind (Span (k, _)) = k; |
24 fun content (Span (_, toks)) = toks; |
25 fun content (Span (_, toks)) = toks; |
|
26 val symbol_length = Position.distance_of o Token.range_of o content; |
25 |
27 |
26 fun position (Span (Command_Span (_, pos), _)) = pos |
28 fun adjust_offsets_kind adjust k = |
27 | position _ = Position.none; |
29 (case k of |
|
30 Command_Span (name, pos) => Command_Span (name, Position.adjust_offsets adjust pos) |
|
31 | _ => k); |
28 |
32 |
29 fun symbol_length span = |
33 fun adjust_offsets adjust (Span (k, toks)) = |
30 (case Position.distance_of (Token.range_of (content span)) of |
34 Span (adjust_offsets_kind adjust k, map (Token.adjust_offsets adjust) toks); |
31 SOME n => n |
|
32 | NONE => raise Fail ("Undefined length of command span" ^ Position.here (position span))); |
|
33 |
35 |
34 end; |
36 end; |