--- a/src/Pure/PIDE/command_span.ML Mon May 14 16:00:10 2018 +0200
+++ b/src/Pure/PIDE/command_span.ML Mon May 14 22:01:00 2018 +0200
@@ -10,8 +10,9 @@
datatype span = Span of kind * Token.T list
val kind: span -> kind
val content: span -> Token.T list
- val position: span -> Position.T
- val symbol_length: span -> int
+ val symbol_length: span -> int option
+ val adjust_offsets_kind: (int -> int option) -> kind -> kind
+ val adjust_offsets: (int -> int option) -> span -> span
end;
structure Command_Span: COMMAND_SPAN =
@@ -22,13 +23,14 @@
fun kind (Span (k, _)) = k;
fun content (Span (_, toks)) = toks;
-
-fun position (Span (Command_Span (_, pos), _)) = pos
- | position _ = Position.none;
+val symbol_length = Position.distance_of o Token.range_of o content;
-fun symbol_length span =
- (case Position.distance_of (Token.range_of (content span)) of
- SOME n => n
- | NONE => raise Fail ("Undefined length of command span" ^ Position.here (position span)));
+fun adjust_offsets_kind adjust k =
+ (case k of
+ Command_Span (name, pos) => Command_Span (name, Position.adjust_offsets adjust pos)
+ | _ => k);
+
+fun adjust_offsets adjust (Span (k, toks)) =
+ Span (adjust_offsets_kind adjust k, map (Token.adjust_offsets adjust) toks);
end;