# HG changeset patch
# User wenzelm
# Date 1218233366 -7200
# Node ID a6da5f68e776205ef261dee462026616372415e1
# Parent  f67f4c677d81d433f95f73e83707cfd61af125f2
added distance_of (permissive version);
added no_range;
tuned;

diff -r f67f4c677d81 -r a6da5f68e776 src/Pure/General/position.ML
--- a/src/Pure/General/position.ML	Fri Aug 08 19:29:01 2008 +0200
+++ b/src/Pure/General/position.ML	Sat Aug 09 00:09:26 2008 +0200
@@ -8,11 +8,12 @@
 signature POSITION =
 sig
   type T
-  val advance: Symbol.symbol -> T -> T
   val line_of: T -> int option
   val column_of: T -> int option
   val offset_of: T -> int option
   val file_of: T -> string option
+  val advance: Symbol.symbol -> T -> T
+  val distance_of: T -> T -> int
   val none: T
   val start: T
   val file: string -> T
@@ -26,6 +27,7 @@
   val report: Markup.T -> T -> unit
   val str_of: T -> string
   type range = T * T
+  val no_range: range
   val encode_range: range -> T
   val reset_range: T -> T
   val range: T -> T -> range
@@ -47,6 +49,15 @@
 fun value k i = if valid i then [(k, string_of_int i)] else [];
 
 
+(* fields *)
+
+fun line_of (Pos ((i, _, _), _)) = if valid i then SOME i else NONE;
+fun column_of (Pos ((_, j, _), _)) = if valid j then SOME j else NONE;
+fun offset_of (Pos ((_, _, k), _)) = if valid k then SOME k else NONE;
+
+fun file_of (Pos (_, props)) = AList.lookup (op =) props Markup.fileN;
+
+
 (* advance *)
 
 fun advance_count "\n" (i: int, j: int, k: int) =
@@ -62,16 +73,12 @@
   if invalid_count count then pos else Pos (advance_count sym count, props);
 
 
-(* fields *)
+(* distance of adjacent positions *)
 
-fun line_of (Pos ((i, _, _), _)) = if valid i then SOME i else NONE;
-fun column_of (Pos ((_, j, _), _)) = if valid j then SOME j else NONE;
-fun offset_of (Pos ((_, _, k), _)) = if valid k then SOME k else NONE;
-
-fun file_of (Pos (_, props)) = AList.lookup (op =) props Markup.fileN;
-
-fun file_name "" = []
-  | file_name name = [(Markup.fileN, name)];
+fun distance_of (Pos ((_, j, k), _)) (Pos ((_, j', k'), _)) =
+  if valid j andalso valid j' then j' - j
+  else if valid k andalso valid k' then k' - k
+  else 0;
 
 
 (* make position *)
@@ -79,6 +86,9 @@
 val none = Pos ((0, 0, 0), []);
 val start = Pos ((1, 1, 1), []);
 
+fun file_name "" = []
+  | file_name name = [(Markup.fileN, name)];
+
 fun file name = Pos ((1, 1, 1), file_name name);
 
 fun line_file i name = Pos ((i, 0, 0), file_name name);
@@ -132,6 +142,8 @@
 
 type range = T * T;
 
+val no_range = (none, none);
+
 fun encode_range (Pos (count, props), Pos ((i, j, k), _)) =
   let val props' = props |> fold_rev (AList.update op =)
     (value Markup.end_lineN i @ value Markup.end_columnN j @ value Markup.end_offsetN k)