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