advance: do not count utf8 trailer bytes (which happen to be undefined or punctuation in iso-latin);
authorwenzelm
Sat, 12 Apr 2008 17:00:47 +0200
changeset 26633 ff317b19e24e
parent 26632 90c0b075c0d3
child 26634 149f80f27c84
advance: do not count utf8 trailer bytes (which happen to be undefined or punctuation in iso-latin);
src/Pure/General/position.ML
--- a/src/Pure/General/position.ML	Sat Apr 12 17:00:47 2008 +0200
+++ b/src/Pure/General/position.ML	Sat Apr 12 17:00:47 2008 +0200
@@ -46,8 +46,9 @@
 val path = file o Path.implode o Path.expand;
 
 fun advance "\n" (Pos (SOME (m, _), props)) = Pos (SOME (m + 1, 1), props)
-  | advance sym (pos as Pos (SOME (m, n), props)) =
-      if Symbol.is_regular sym then Pos (SOME (m, n + 1), props) else pos
+  | advance s (pos as Pos (SOME (m, n), props)) =
+      if Symbol.is_regular s andalso not (Symbol.is_utf8_trailer s)
+      then Pos (SOME (m, n + 1), props) else pos
   | advance _ pos = pos;