adjust position according to offset of command/exec id;
authorwenzelm
Mon May 14 22:01:00 2018 +0200 (12 months ago)
changeset 681836560324b1e4d
parent 68182 fa3cf61121ee
child 68184 6c693b2700b3
adjust position according to offset of command/exec id;
src/Pure/General/position.ML
src/Pure/Isar/token.ML
src/Pure/PIDE/command_span.ML
     1.1 --- a/src/Pure/General/position.ML	Mon May 14 16:00:10 2018 +0200
     1.2 +++ b/src/Pure/General/position.ML	Mon May 14 22:01:00 2018 +0200
     1.3 @@ -14,7 +14,7 @@
     1.4    val end_offset_of: T -> int option
     1.5    val file_of: T -> string option
     1.6    val advance: Symbol.symbol -> T -> T
     1.7 -  val advance_offset: int -> T -> T
     1.8 +  val advance_offsets: int -> T -> T
     1.9    val distance_of: T * T -> int option
    1.10    val none: T
    1.11    val start: T
    1.12 @@ -30,6 +30,7 @@
    1.13    val get_id: T -> string option
    1.14    val put_id: string -> T -> T
    1.15    val parse_id: T -> int option
    1.16 +  val adjust_offsets: (int -> int option) -> T -> T
    1.17    val of_properties: Properties.T -> T
    1.18    val properties_of: T -> Properties.T
    1.19    val offset_properties_of: T -> Properties.T
    1.20 @@ -104,10 +105,11 @@
    1.21  fun advance sym (pos as (Pos (count, props))) =
    1.22    if invalid_count count then pos else Pos (advance_count sym count, props);
    1.23  
    1.24 -fun advance_offset offset (pos as (Pos (count as (i, j, k), props))) =
    1.25 -  if invalid_count count then pos
    1.26 +fun advance_offsets offset (pos as (Pos (count as (i, j, k), props))) =
    1.27 +  if offset = 0 orelse invalid_count count then pos
    1.28 +  else if offset < 0 then raise Fail "Illegal offset"
    1.29    else if valid i then raise Fail "Illegal line position"
    1.30 -  else Pos ((i, if_valid j (j + offset), k), props);
    1.31 +  else Pos ((i, if_valid j (j + offset), if_valid k (k + offset)), props);
    1.32  
    1.33  
    1.34  (* distance of adjacent positions *)
    1.35 @@ -143,6 +145,17 @@
    1.36  fun parse_id pos = Option.map Value.parse_int (get_id pos);
    1.37  
    1.38  
    1.39 +fun adjust_offsets adjust (pos as Pos (_, props)) =
    1.40 +  (case parse_id pos of
    1.41 +    SOME id =>
    1.42 +      (case adjust id of
    1.43 +        SOME offset =>
    1.44 +          let val Pos (count, _) = advance_offsets offset pos
    1.45 +          in Pos (count, Properties.remove Markup.idN props) end
    1.46 +      | NONE => pos)
    1.47 +  | NONE => pos);
    1.48 +
    1.49 +
    1.50  (* markup properties *)
    1.51  
    1.52  fun get props name =
     2.1 --- a/src/Pure/Isar/token.ML	Mon May 14 16:00:10 2018 +0200
     2.2 +++ b/src/Pure/Isar/token.ML	Mon May 14 22:01:00 2018 +0200
     2.3 @@ -31,6 +31,7 @@
     2.4      Files of file Exn.result list
     2.5    val pos_of: T -> Position.T
     2.6    val range_of: T list -> Position.range
     2.7 +  val adjust_offsets: (int -> int option) -> T -> T
     2.8    val eof: T
     2.9    val is_eof: T -> bool
    2.10    val not_eof: T -> bool
    2.11 @@ -192,6 +193,9 @@
    2.12        in Position.range (pos_of tok, pos') end
    2.13    | range_of [] = Position.no_range;
    2.14  
    2.15 +fun adjust_offsets adjust (Token ((x, range), y, z)) =
    2.16 +  Token ((x, apply2 (Position.adjust_offsets adjust) range), y, z);
    2.17 +
    2.18  
    2.19  (* stopper *)
    2.20  
    2.21 @@ -681,7 +685,7 @@
    2.22  
    2.23  fun make ((k, n), s) pos =
    2.24    let
    2.25 -    val pos' = Position.advance_offset n pos;
    2.26 +    val pos' = Position.advance_offsets n pos;
    2.27      val range = Position.range (pos, pos');
    2.28      val tok =
    2.29        if 0 <= k andalso k < Vector.length immediate_kinds then
     3.1 --- a/src/Pure/PIDE/command_span.ML	Mon May 14 16:00:10 2018 +0200
     3.2 +++ b/src/Pure/PIDE/command_span.ML	Mon May 14 22:01:00 2018 +0200
     3.3 @@ -10,8 +10,9 @@
     3.4    datatype span = Span of kind * Token.T list
     3.5    val kind: span -> kind
     3.6    val content: span -> Token.T list
     3.7 -  val position: span -> Position.T
     3.8 -  val symbol_length: span -> int
     3.9 +  val symbol_length: span -> int option
    3.10 +  val adjust_offsets_kind: (int -> int option) -> kind -> kind
    3.11 +  val adjust_offsets: (int -> int option) -> span -> span
    3.12  end;
    3.13  
    3.14  structure Command_Span: COMMAND_SPAN =
    3.15 @@ -22,13 +23,14 @@
    3.16  
    3.17  fun kind (Span (k, _)) = k;
    3.18  fun content (Span (_, toks)) = toks;
    3.19 -
    3.20 -fun position (Span (Command_Span (_, pos), _)) = pos
    3.21 -  | position _ = Position.none;
    3.22 +val symbol_length = Position.distance_of o Token.range_of o content;
    3.23  
    3.24 -fun symbol_length span =
    3.25 -  (case Position.distance_of (Token.range_of (content span)) of
    3.26 -    SOME n => n
    3.27 -  | NONE => raise Fail ("Undefined length of command span" ^ Position.here (position span)));
    3.28 +fun adjust_offsets_kind adjust k =
    3.29 +  (case k of
    3.30 +    Command_Span (name, pos) => Command_Span (name, Position.adjust_offsets adjust pos)
    3.31 +  | _ => k);
    3.32 +
    3.33 +fun adjust_offsets adjust (Span (k, toks)) =
    3.34 +  Span (adjust_offsets_kind adjust k, map (Token.adjust_offsets adjust) toks);
    3.35  
    3.36  end;