clarified signature;
authorwenzelm
Mon May 14 09:39:27 2018 +0200 (12 months ago)
changeset 681776e40f5d43936
parent 68174 7c4793e39dd5
child 68178 e3dd94d04eee
clarified signature;
more operations;
src/Pure/General/position.ML
src/Pure/General/symbol_pos.ML
src/Pure/PIDE/command_span.ML
     1.1 --- a/src/Pure/General/position.ML	Sun May 13 21:59:41 2018 +0200
     1.2 +++ b/src/Pure/General/position.ML	Mon May 14 09:39:27 2018 +0200
     1.3 @@ -15,7 +15,7 @@
     1.4    val file_of: T -> string option
     1.5    val advance: Symbol.symbol -> T -> T
     1.6    val advance_offset: int -> T -> T
     1.7 -  val distance_of: T -> T -> int
     1.8 +  val distance_of: T * T -> int option
     1.9    val none: T
    1.10    val start: T
    1.11    val file_name: string -> Properties.T
    1.12 @@ -112,9 +112,8 @@
    1.13  
    1.14  (* distance of adjacent positions *)
    1.15  
    1.16 -fun distance_of (Pos ((_, j, _), _)) (Pos ((_, j', _), _)) =
    1.17 -  if valid j andalso valid j' then j' - j
    1.18 -  else 0;
    1.19 +fun distance_of (Pos ((_, j, _), _), Pos ((_, j', _), _)) =
    1.20 +  if valid j andalso valid j' then SOME (j' - j) else NONE;
    1.21  
    1.22  
    1.23  (* make position *)
     2.1 --- a/src/Pure/General/symbol_pos.ML	Sun May 13 21:59:41 2018 +0200
     2.2 +++ b/src/Pure/General/symbol_pos.ML	Mon May 14 09:39:27 2018 +0200
     2.3 @@ -244,7 +244,7 @@
     2.4    | pad ((s1, pos1) :: (rest as (_, pos2) :: _)) =
     2.5        let
     2.6          val end_pos1 = Position.advance s1 pos1;
     2.7 -        val d = Int.max (0, Position.distance_of end_pos1 pos2);
     2.8 +        val d = Int.max (0, the_default 0 (Position.distance_of (end_pos1, pos2)));
     2.9        in s1 :: replicate d Symbol.DEL @ pad rest end;
    2.10  
    2.11  val implode = implode o pad;
     3.1 --- a/src/Pure/PIDE/command_span.ML	Sun May 13 21:59:41 2018 +0200
     3.2 +++ b/src/Pure/PIDE/command_span.ML	Mon May 14 09:39:27 2018 +0200
     3.3 @@ -10,6 +10,8 @@
     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  end;
    3.10  
    3.11  structure Command_Span: COMMAND_SPAN =
    3.12 @@ -21,4 +23,12 @@
    3.13  fun kind (Span (k, _)) = k;
    3.14  fun content (Span (_, toks)) = toks;
    3.15  
    3.16 +fun position (Span (Command_Span (_, pos), _)) = pos
    3.17 +  | position _ = Position.none;
    3.18 +
    3.19 +fun symbol_length span =
    3.20 +  (case Position.distance_of (Token.range_of (content span)) of
    3.21 +    SOME n => n
    3.22 +  | NONE => raise Fail ("Undefined length of command span" ^ Position.here (position span)));
    3.23 +
    3.24  end;