--- a/src/Pure/PIDE/command_span.ML Sat Nov 28 13:49:46 2020 +0100
+++ b/src/Pure/PIDE/command_span.ML Sat Nov 28 14:25:27 2020 +0100
@@ -6,6 +6,7 @@
signature COMMAND_SPAN =
sig
+ val extensions: string list -> Path.T -> Path.T list
datatype kind = Command_Span of string * Position.T | Ignored_Span | Malformed_Span
datatype span = Span of kind * Token.T list
val kind: span -> kind
@@ -18,6 +19,13 @@
structure Command_Span: COMMAND_SPAN =
struct
+(* loaded files *)
+
+fun extensions exts path = map (fn ext => Path.ext ext path) exts;
+
+
+(* span *)
+
datatype kind = Command_Span of string * Position.T | Ignored_Span | Malformed_Span;
datatype span = Span of kind * Token.T list;
@@ -25,6 +33,9 @@
fun content (Span (_, toks)) = toks;
val symbol_length = Position.distance_of o Token.range_of o content;
+
+(* presentation positions *)
+
fun adjust_offsets_kind adjust k =
(case k of
Command_Span (name, pos) => Command_Span (name, Position.adjust_offsets adjust pos)