--- a/src/Pure/PIDE/command_span.ML Sun May 13 21:59:41 2018 +0200
+++ b/src/Pure/PIDE/command_span.ML Mon May 14 09:39:27 2018 +0200
@@ -10,6 +10,8 @@
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
end;
structure Command_Span: COMMAND_SPAN =
@@ -21,4 +23,12 @@
fun kind (Span (k, _)) = k;
fun content (Span (_, toks)) = toks;
+fun position (Span (Command_Span (_, pos), _)) = pos
+ | position _ = Position.none;
+
+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)));
+
end;