# HG changeset patch
# User wenzelm
# Date 1526283567 -7200
# Node ID 6e40f5d4393672854da4b284760f36b91c3ee121
# Parent  7c4793e39dd54d797d87c554bd3d2f804c932f03
clarified signature;
more operations;

diff -r 7c4793e39dd5 -r 6e40f5d43936 src/Pure/General/position.ML
--- a/src/Pure/General/position.ML	Sun May 13 21:59:41 2018 +0200
+++ b/src/Pure/General/position.ML	Mon May 14 09:39:27 2018 +0200
@@ -15,7 +15,7 @@
   val file_of: T -> string option
   val advance: Symbol.symbol -> T -> T
   val advance_offset: int -> T -> T
-  val distance_of: T -> T -> int
+  val distance_of: T * T -> int option
   val none: T
   val start: T
   val file_name: string -> Properties.T
@@ -112,9 +112,8 @@
 
 (* distance of adjacent positions *)
 
-fun distance_of (Pos ((_, j, _), _)) (Pos ((_, j', _), _)) =
-  if valid j andalso valid j' then j' - j
-  else 0;
+fun distance_of (Pos ((_, j, _), _), Pos ((_, j', _), _)) =
+  if valid j andalso valid j' then SOME (j' - j) else NONE;
 
 
 (* make position *)
diff -r 7c4793e39dd5 -r 6e40f5d43936 src/Pure/General/symbol_pos.ML
--- a/src/Pure/General/symbol_pos.ML	Sun May 13 21:59:41 2018 +0200
+++ b/src/Pure/General/symbol_pos.ML	Mon May 14 09:39:27 2018 +0200
@@ -244,7 +244,7 @@
   | pad ((s1, pos1) :: (rest as (_, pos2) :: _)) =
       let
         val end_pos1 = Position.advance s1 pos1;
-        val d = Int.max (0, Position.distance_of end_pos1 pos2);
+        val d = Int.max (0, the_default 0 (Position.distance_of (end_pos1, pos2)));
       in s1 :: replicate d Symbol.DEL @ pad rest end;
 
 val implode = implode o pad;
diff -r 7c4793e39dd5 -r 6e40f5d43936 src/Pure/PIDE/command_span.ML
--- a/src/Pure/PIDE/command_span.ML	Sun May 13 21:59:41 2018 +0200
+++ b/src/Pure/PIDE/command_span.ML	Mon May 14 09:39:27 2018 +0200
@@ -10,6 +10,8 @@
   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
 end;
 
 structure Command_Span: COMMAND_SPAN =
@@ -21,4 +23,12 @@
 fun kind (Span (k, _)) = k;
 fun content (Span (_, toks)) = toks;
 
+fun position (Span (Command_Span (_, pos), _)) = pos
+  | position _ = Position.none;
+
+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)));
+
 end;