The Coq mailing list

[Abhishek Anand <abhishek.anand.iitg AT gmail.com>]

Thanks. Indeed, Rodolphe Lepigre just suggested doing
goto-char (position-bytes (pos-computed-from-glob-file)) instead of  goto-char (pos-computed-from-glob-file) and it works. Issue closed.

Thanks

-- Abhishek

http://www.cs.cornell.edu/~aa755/

On Thu, Mar 23, 2023 at 1:09 PM Jim Fehrle <jim.fehrle AT gmail.com> wrote:

The parser returns byte offsets, not Unicode offsets.  Not sure we'd rush to change that--it could be significant work and it would disrupt existing code that relies on byte offsets.  It would be odd to use a different convention for offsets just for .glob.  In code such as your .glob-file based jump to definition, it shouldn't be hard to convert from a byte offset to a unicode offset.

On Thu, Mar 23, 2023 at 9:43 AM Abhishek Anand <abhishek.anand.iitg AT gmail.com> wrote:

When I tell emacs to jump at character offset 56 (using (goto-char 56)) in A.v, it goes to the 

whitespace character just after "Lemma" in A.v, which is correct, e.g. when using for "jump to definition" of xx.

But when I start using unicode characters, this gets messed up.

Is there a way to get coqc to produce the "correct" offsets in .glob files:where it doesnt count unicode characters as multiple files?

Alternatively, is there some variant in goto-char in emacs that can account for the double counting of unicode characters?

-- Abhishek

http://www.cs.cornell.edu/~aa755/