adjust position according to offset of command/exec id;

--- a/src/Pure/General/position.ML	Mon May 14 16:00:10 2018 +0200
+++ b/src/Pure/General/position.ML	Mon May 14 22:01:00 2018 +0200
@@ -14,7 +14,7 @@
   val end_offset_of: T -> int option
   val file_of: T -> string option
   val advance: Symbol.symbol -> T -> T
-  val advance_offset: int -> T -> T
+  val advance_offsets: int -> T -> T
   val distance_of: T * T -> int option
   val none: T
   val start: T
@@ -30,6 +30,7 @@
   val get_id: T -> string option
   val put_id: string -> T -> T
   val parse_id: T -> int option
+  val adjust_offsets: (int -> int option) -> T -> T
   val of_properties: Properties.T -> T
   val properties_of: T -> Properties.T
   val offset_properties_of: T -> Properties.T
@@ -104,10 +105,11 @@
 fun advance sym (pos as (Pos (count, props))) =
   if invalid_count count then pos else Pos (advance_count sym count, props);
 
-fun advance_offset offset (pos as (Pos (count as (i, j, k), props))) =
-  if invalid_count count then pos
+fun advance_offsets offset (pos as (Pos (count as (i, j, k), props))) =
+  if offset = 0 orelse invalid_count count then pos
+  else if offset < 0 then raise Fail "Illegal offset"
   else if valid i then raise Fail "Illegal line position"
-  else Pos ((i, if_valid j (j + offset), k), props);
+  else Pos ((i, if_valid j (j + offset), if_valid k (k + offset)), props);
 
 
 (* distance of adjacent positions *)
@@ -143,6 +145,17 @@
 fun parse_id pos = Option.map Value.parse_int (get_id pos);
 
 
+fun adjust_offsets adjust (pos as Pos (_, props)) =
+  (case parse_id pos of
+    SOME id =>
+      (case adjust id of
+        SOME offset =>
+          let val Pos (count, _) = advance_offsets offset pos
+          in Pos (count, Properties.remove Markup.idN props) end
+      | NONE => pos)
+  | NONE => pos);
+
+
 (* markup properties *)
 
 fun get props name =

--- a/src/Pure/Isar/token.ML	Mon May 14 16:00:10 2018 +0200
+++ b/src/Pure/Isar/token.ML	Mon May 14 22:01:00 2018 +0200
@@ -31,6 +31,7 @@
     Files of file Exn.result list
   val pos_of: T -> Position.T
   val range_of: T list -> Position.range
+  val adjust_offsets: (int -> int option) -> T -> T
   val eof: T
   val is_eof: T -> bool
   val not_eof: T -> bool
@@ -192,6 +193,9 @@
       in Position.range (pos_of tok, pos') end
   | range_of [] = Position.no_range;
 
+fun adjust_offsets adjust (Token ((x, range), y, z)) =
+  Token ((x, apply2 (Position.adjust_offsets adjust) range), y, z);
+
 
 (* stopper *)
 
@@ -681,7 +685,7 @@
 
 fun make ((k, n), s) pos =
   let
-    val pos' = Position.advance_offset n pos;
+    val pos' = Position.advance_offsets n pos;
     val range = Position.range (pos, pos');
     val tok =
       if 0 <= k andalso k < Vector.length immediate_kinds then

--- 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;