--- 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)