# HG changeset patch
# User berghofe
# Date 1295127617 -3600
# Node ID 2b07a4212d6d55a08c0e05d652f2fe047de8d08a
# Parent  12910b69684fcbedca92aac555b2b4826cbbff97
Replaced ad-hoc advance function by Position.advance

diff -r 12910b69684f -r 2b07a4212d6d src/HOL/SPARK/Tools/fdl_lexer.ML
--- a/src/HOL/SPARK/Tools/fdl_lexer.ML	Sat Jan 15 21:24:15 2011 +0100
+++ b/src/HOL/SPARK/Tools/fdl_lexer.ML	Sat Jan 15 22:40:17 2011 +0100
@@ -74,25 +74,6 @@
 
 type chars = (string * Position.T) list;
 
-(* a variant of Position.advance (see Pure/General/position.ML) *)
-fun advance x pos =
-  let
-    fun incr i = i+1;
-    fun change_prop s f props = case Properties.get_int props s of
-        NONE => props
-      | SOME i => Properties.put (s, Int.toString (f i)) props;
-  in
-    pos |>
-    Position.properties_of |>
-    change_prop "offset" incr |>
-    (case x of
-       "\n" =>
-         change_prop "line" incr #>
-         change_prop "column" (K 1)
-     | _ => change_prop "column" incr) |>
-    Position.of_properties
-  end;
-
 fun is_char_eof ("", _) = true
   | is_char_eof _ = false;
 
@@ -101,7 +82,7 @@
 fun symbol (x : string, _ : Position.T) = x;
 
 fun explode_pos s pos = fst (fold_map (fn x => fn pos =>
-  ((x, pos), advance x pos)) (raw_explode s) pos);
+  ((x, pos), Position.advance x pos)) (raw_explode s) pos);
 
 
 (** scanners **)