The Coq mailing list

[Stefan Monnier <monnier AT iro.umontreal.ca>]

> Is there a way to get coqc to produce the "correct" offsets in .glob
> files:where it doesnt count unicode characters as multiple chars?
> Alternatively, is there some variant in goto-char in Emacs that can account
> for the double counting of unicode characters?

You need to convert between "bytes in the file" and "chars in Emacs
buffer".  The conversion between the two depends on the
coding-system used and can be non-trivial.

When you use `byte-to-position` you convert between "bytes in Emacs
buffer" and "chars in Emacs buffer" which is not quite the same.
In many cases this will happen to work right, tho: Emacs's internal
representation is a variant of UTF-8, so if your file's coding-system is
also UTF-8 the two will usually coincide but if your file uses something
different then you're out of luck.

If you want to convert between a file's byte-positions and its buffer's
char positions you want `filepos-to-bufferpos` and `bufferpos-to-filepos`.

Note also that all those functions counts bytes (and chars) from the
beginning of the buffer rather than from the beginning of the line, so
you will probably want to do a gymnastics like

    (defun my-goto-line-byte (bytes)
      (let* ((bolc (line-beginning-position))
             (bolb (bufferpos-to-filepos bolc))
             (targetb (+ bolb bytes))
             (targetc (filepos-to-bufferpos targetb)))
        (goto-char targetc)))

Another option is to do something like:

    (defun my-goto-line-byte (bytes)
      (goto-char (line-beginning-position))
      (let* ((linec (buffer-substring (point) (line-end-position)))
             (lineb (encode-coding-string line buffer-file-coding-system))
             (prefixb (substring lineb 0 bytes))
             (prefixc (decode-coding-string lineb buffer-file-coding-system)))
        (forward-char (length prefixc))))

This last option is fundamentally the only "reliable" option, and the
`filepos<->bufferpos` functions may en up using such a thing internally
(and if so, encoding/decoding the whole freaking buffer, thus making
this operation O(buffer-size) :-( ).


        Stefan