# HG changeset patch # User wenzelm # Date 1526328060 -7200 # Node ID 6560324b1e4dc36b5323040262b57e8bda09e97c # Parent fa3cf61121ee0bdf958770e11fb90c8ead229139 adjust position according to offset of command/exec id; diff -r fa3cf61121ee -r 6560324b1e4d src/Pure/General/position.ML --- 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 = diff -r fa3cf61121ee -r 6560324b1e4d src/Pure/Isar/token.ML --- 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 diff -r fa3cf61121ee -r 6560324b1e4d src/Pure/PIDE/command_span.ML --- 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;