1(*  Title:      Pure/PIDE/command_span.ML
2    Author:     Makarius
3
4Syntactic representation of command spans.
5*)
6
7signature COMMAND_SPAN =
8sig
9  datatype kind = Command_Span of string * Position.T | Ignored_Span | Malformed_Span
10  datatype span = Span of kind * Token.T list
11  val kind: span -> kind
12  val content: span -> Token.T list
13  val symbol_length: span -> int option
14  val adjust_offsets_kind: (int -> int option) -> kind -> kind
15  val adjust_offsets: (int -> int option) -> span -> span
16end;
17
18structure Command_Span: COMMAND_SPAN =
19struct
20
21datatype kind = Command_Span of string * Position.T | Ignored_Span | Malformed_Span;
22datatype span = Span of kind * Token.T list;
23
24fun kind (Span (k, _)) = k;
25fun content (Span (_, toks)) = toks;
26val symbol_length = Position.distance_of o Token.range_of o content;
27
28fun adjust_offsets_kind adjust k =
29  (case k of
30    Command_Span (name, pos) => Command_Span (name, Position.adjust_offsets adjust pos)
31  | _ => k);
32
33fun adjust_offsets adjust (Span (k, toks)) =
34  Span (adjust_offsets_kind adjust k, map (Token.adjust_offsets adjust) toks);
35
36end;
37