coq-club AT inria.fr
Subject: The Coq mailing list
List archive
Re: [Coq-Club] correct offsets in .glob files when unicode characters are present
Chronological Thread
- From: Jim Fehrle <jim.fehrle AT gmail.com>
- To: coq-club AT inria.fr
- Subject: Re: [Coq-Club] correct offsets in .glob files when unicode characters are present
- Date: Thu, 23 Mar 2023 10:09:39 -0700
- Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=jim.fehrle AT gmail.com; spf=Pass smtp.mailfrom=jim.fehrle AT gmail.com; spf=None smtp.helo=postmaster AT mail-wr1-f44.google.com
- Ironport-data: A9a23:yYLzQKDdeb0cYxVW///nw5YqxClBgxIJ4kV8jS/XYbTApDIh0GZTy 2cWXWiPOfqPNDOjfY1wO9mz80kGvJPRx9AyOVdlrnsFo1Bi+ZOUX4zBRqvTF3rPdZObFBoPA +E2MISowBUcFyeEzvuVGuG96yM6j8lkf5KkYMbcICd9WAR4fykojBNnioYRj5Vh6TSDK1rlV eja/ouOaDdJ5xYuajhPs/nZ80s11BjPkGpwUmIWNagjUGD2zCF94KI3fcmZM3b+S49IKe+2L 86rIGaRows1Vz90Yj+Uuu6Tnn8iGtY+DiDS4pZiYJVOtzAZzsAEPgnXA9JHAatfo23hc9mcU 7yhv7ToIesiFvWkdOjwz3C0usyxVEFL0OavHJSxjSCc5xXjQibin/5ONXkZGdAg5cEtLnhl8 MVNfVjhbjjb7w636LeyS+0pmd56ace3YMUQvXZvyTyfBvEjKXzBa/+StJkIgXFq3JkIQaq2i 8kxMVKDaDzCYhgJNFoXEpYztOitj3j7NTZfrTp5oIJqujCNk1Usi9ABNvL0Ktuba9xv2XqGo 3zU2XqlWxQwbp+2nG/tHnWE37eTx0sXQrk6H7qhs/VunVe73X0WEBRQVF2hoPD/hFTWZj5EA 0kd+y5rsrJrsUL3Ep/yWBq3pHPCtRkZMzZNLwEkwFmo+/favw25P1AramN5d/t8m9YdQAV/g zdlgOjVLTBotbSUT1eU+bGVsS6+NEApwYkqNX9soewts4mLnW0jsv7cZo08T/Pt37UZDRm1k m/a9nFv71kGpZdTj/3TwLzRv967SnH0ouMd4wzWWie69Fo8atL5IYOv7lff4LBLK4Pxori9U JosypH2AAMmV8nleMmxrAMlQurBCxGtbme0vLKXN8N9nwlBAlb6FWyq3BlwJV1yLuEPciLzb UnYtGt5vcEMbSbyPP8sPdPpU6zGKJQM8/y1Bpg4ifIeMvBMmPOvoUmCmGbKjjuzwBV0+U3BE cvHKZnE4Ykm5VRPlWLqHY/xIJckwScxwW67eHwI50XP7FZqX1bMEe1tGALWPogRtfrYyC2Ir Ys3H5bVk313DreiCgGJqtV7BQ5RfRAG6WXe8pI/mhirflc8SAnMypb5ndscRmCSt/8KzruVp i/hCxAwJZiWrSSvFDhmo0tLMNvHNauTZ1piVcD1FQfzgyoQcsy04b0BdpA6W7Ai+aYxhbR3V vQJMYHISPhGVj2NqXxXYIjfvb5SUk2hpTuPGC65Pxk5XZprHDLS9vHeIwDAySgpDwiMj/UYn YGO7A3gbKQmexVDF+fTMfKm8EOwtyMSmcV0REr5HeNQc0TNrqlvciz4seArL5otOTH892O8/ FuQC01Jo+PinpIEqojVpKGbrrWGF/l1MVpaElL6s5e3F3j+1UiyzbBQVN2neWjma1r136G5d 8B5/urZMsBbrG1VsoF5Laln/Zg+6/TrubVe6AZuR1fPUHiGFZJiJSOg8fRUl6gQ2IJchxS6a niP9vZeJ7+NHsHvS3wVBQg9a9W8xeMmoSbT4ds1MXfFyndOppTfanprPj6IlCB5B5l2Otl8w e4e5egn2zbmgR8uatu7niRY8lqXFUM5UoIliMA+IJTqgQ8V2F19ccTiKivp0qquNfRIEGcXe wGxuoSTqYhY9ET4d1gLKUPsxstY3JQHhwBLxgQNJnOPgdv0ucU01xxwrxUyQhhk8RFc9+dVJ GJQFlZUIJ+W9GxCn/lzXGGLGiBACiaG+0f39UA7qW3BQ2SsVU3PNGcYO9vR2Gw87ERnYWF90 JyD7WTqQxLGXZvU5TQjf1xhp9jIb81DxieblO+JR826ToQHOxz7iaqQVE80ghrAA+ZqoWbYp ONvrd1CWYeiOQE++6QEWpSnj5IOQxW5JUtHc/Fr3IUNOUr+IDiS+zy/G3qdS/N3Bc7h0BGHU pR1B8d1SR6B+j6ErWkbCY4yMrZEpqMVy+RYSIz7B1wtkuW5nmJyvYPy5xrOojYhY+9TnPYXL qLTcDO/EVKsu0ZEpl+VrOR5PjuXXNpVQiz9w+G/z8sRHb0hruxHUB8/w5m0jVqvISpl+BOm5 lrDbpDJ0t04mJhNnpTtIIpHFQ6bOdP+b8XW0QGR4vBlT8LDDtfKjCwR8mLYBgVxOaAAfeh4j pGfmYfT8H6dmY0pQkf1voKkFZhZwemTB81patnWKltelgu8AP7c2QMJoT2EGMYYgeFj6dmCb CrmTdm7avo+ecpXnV9RYAhgSyctMbz9NPrclHnsvsa3K0Yv1CLcJ4ma7l7vV2ZQcxEIN7DYC gPZv/WP5MhSnL9TBS0rVu1XPJtlHGDNAacWVcX9lT29PFmahlmvvrjDlx155w+SWzPAWIz/7 IneTxfzSAWqteuahJtFuoh1pVsMAGw7neA0eVkH9sVrjyyhSlQLNvkZLY5MH6Q8fvYeD30kT GqlgKoe5STBsfBsdBz95JH8RF7aCLBSfNj+ITMt8gWfbCLe6EZsxld+3n8I3pu0UmKLICKbx RU29Xj5Pxz3yZZsLQrWzuLumv9pn5s22VpRkX0QUKXO79I2DrAD1XgnFw1IPcAC/wchi22TT VUIqat4rI1XhKI//QuMu5KYJf3BgA7S8g==
- Ironport-hdrordr: A9a23:9sgHhKoHpsCnI8XRpnNmee0aV5o8eYIsimQD101hICG9Afbo8v xG/c5rtiMc5wx+ZJhNo7q90cq7IU80l6QV3WB5B97LNzUOl1HEEGgI1+TfKkjbaknDH4BmuZ uIC5IOauHNMQ==
- Ironport-phdr: A9a23:egKzLxfaSf3NBSOGUgIOA96ClGM+iNTLVj580XLHo4xHfqnrxZn+J kuXvawr0AWUG9+Ht7kV1qL/iOPJZy8p2d65qncMcZhBBVcuqP49uEgeOvODElDxN/XwbiY3T 4xoXV5h+GynYwAOQJ6tL1LdrWev4jEMBx7xKRR6JvjvGo7Vks+7y/2+94fcbglWhDexe61+I Rq5oAnessQbgZZpJ7osxBfOvnZHdONayH9yK1mOhRj8/MCw/JBi8yRUpf0s8tNLXLv5caolU 7FWFSwqPG8p6sLlsxnDVhaP6WAHUmoKiBpIAhPK4w/8U5zsryb1rOt92C2dPc3rUbA5XCmp4 ql3RBP0jioMKjg0+3zVhMNtlqJWuB2upxJ9zIDUbo+bN+dwcL3Bct4BX2VNQtxcWjZdDo+gb YYCCfcKM+ZCr4n6olsDtR+wBQipBOjyyjFHmH/23bc+0+s/DArL2w4gH9MLsHjOotX6KqcSU fqxzKbW1jjDYPZW1i386IjMaBwuvfaMXbdpfMfX1EIgGB/LgE+Kpoz5IzOayP4Ns26D4ud8V eyil3Irpg9yrzWz2MshlJfEi5wIx13a8Sh13YU4KN+lRUB0fNOoDZReuS6eOoZoQs0vX39lt Sg0xLAFpZK2ejUBxpogxx7acfOHco6I7wr/W+aWOzd4gmxqeLa7hxqo70ev1/D8W8+p21hJt ipIisfAumwJ2hDJ6cWKSuFx8lm/1TqSzQze5e5JLEYpnqTBMZEh2KQ/lp8LvETDACD2nEL2g beTdko+++io7/3rY7v8ppOBLoN0hA7zP6s0lsywBuQ4NQcOX2yF9uimyLLj+kj5TK1Ljv0wj KbZrIjXKdoHqqO9GQNY0YYu5wyhAzu4zdgUh3YKIV1ddBKClYfpOlXOIP7iDfe4hlShiDVrx /HDPrH7DJXCMHjDkK3lfblj8ENcxw8zwspe55JQEL0OPPXzWkrpuNzeFRA2Kxa0zPr/CNVhy oMeXnqCDrKBPKPIrVCI/v4vI/WLZIINpDn9LOEl6+fygn89hF8SZrKk3YAXaXC9BvRpOV+VY XvqgtcbEGcFpBAyTOLwiA7KbTkGbHGrGqk4+zsTCYS8DI6FSJr+rqaG2XKZH5geSG1GEFSBW SPqdoDCVfoMciafCsBkmz0AE7OmTtlyhlmVqAbmxu8/faLv8SoCuMe7vDAUz+jalBVpsCdxE 9zYyGaVCWd9gmIPQTYymqF5u010jFmZguBjm/INM9tV6rtSVxsic4bGxrl4CtW0VA/BZNOEY FmjS9SiRzo2S4F52McANn50AM7qlRXfx2yvCr4RmaaMAck286ea0XXxPcJw43nD3aglyVIhR 5gHLnWo04h48QWbHIvViwOZmqKtILwbxzLI/XyfwHCmuUhZVEtvS/yAUyxDIETRqtv96wXJS LrG5a0PFAxHxIbCL6JLboasllBaXLL4P8yYZWutmmC2DBLOx7WWbYOsdX9PlCPaQFMJlQwe5 xPkfUA3GzuhrmTCDTdvCUOnYkXi9vN7oW+6SUl8xh+Dbklo3b64shAPgvnUR/QW17MC8CAvz lc8VFS82pTYBtqaowdJc6BVYNd761BClCrYuwF7Ip28PvV6nFdNOw9zvk7oy1B2EtAayZls/ C5sllArb/7EgzYjP3uC0Jv9O6PaMDz39RGrMOvN303Glc2R4uEJ4eg5rFPquEeoEFAj+jNpy YowsTPU65PUAQ4VSZ+0XFww8k0wpbDfJCcw55nQ2FVjNKC1tnnJ3NdjV45Hgl6wOsxSNq+JD lq4EcwfQcajKPYulnCmaxsFOKZZ86t+bKbEP7OWnaWsOuhnhjevi29KtZt83ky7/C15UufU3 pwBzpl0xyO/XiznxBeku8HzwsVfYC0KW3G40W7iDZJQYat7ecAKD32vKou53Ic2i5noUn9ev FmtYjFOkM2ofFycYlzn2QB42kEeoHjhkiy9hzB5iDAmqKOD0TeGmbyzMkpafDQRHS8+0R/lO sCsgsofXVS0YgRM9lPt/kv8y6VB5ex+I2TVXUZUbn3zJmBmXLG3s+nKaMpO5ZU09CRPBb7kM BbKF/in+UJcj3+wegkWjCo2fDyrpJjjyhlziWbGaW12sGKcYsZogxHW+N3bQ/dVmDsAXihxz zfNVT3ed5Gk+8uZk5Dbv6WwTWWkA9dRcCytw46Ari+2zWJvCBy72fu0n5e0dGpymT++zNRsW SjS+Vz+Y4yt2am6K+ZqVkZtDV74rcF9H8st9+l4zIFV0n8ciJKP+HMBmmqmKtRX15X1a38VT CIKydrYs0D1nVduJXWTy8flR22Ql4F/MsKibDpciUdfp4haTb2Z57tekW5pr0qk+EjPNONlk G5VyONyuiVHxbhY4Ex3knrbWvdIQQFZJXC+yUjOtYvl6vwJPCD3NuHhsSg21dG5UOPc/EcFA Cy/ItF6WnUopsRnbACSjjupttCiKIGWNZVJ7lWVi0uS0LITcc53z6tQw3IgYDKY3zVtyvZn3 0Mym8jg4c7fbT0qpfzxAwYEZGStN4VKpW6r3eAG2ZzPl4G3Qsc4RW5NBcq0C6ruSHVL65GFf 06PCGFu8C/KX+qCW1bFuAE+6CuQW5GzayPNfSdfkIUkHUjHYhQY2VFcXS1mzMRgSEbwn52nK x0/vndItzua4lNaw+ZsfXETS0/5owGlIncxQZmbd19N6x1aolzSKYqY5/5yGCdR+tugqhaMI yqVfVYAC2ZBQUGCC135W9vmrdDd7+iVAPa/JPrScP2Pr+JZTfKB2ZOo1MNv4T+NMsyFOnQqA ec83wJPWnVwGsKRnDtqKWRfjyXWc8uSvwux4AVyp8G7tevxAUfhudfJBLxVPtFivRuxhObLN uKdgjp4NScN1p4IwiytqvBX11oThidyMji1RO5Y5GidEeSKwPYRU0JIDkE7fNFF5K89wARXb MvSi9euk6V9kuZwEFBdE1rohsCuY8UOZWC7LlLOQkiRZ9HkbXXGxd/6ZaSkRPheluJR4leyu DPdHULjJDCOvzbsXhGrd+pLiWvIWX4W8JH4aRtrBWX5GZj+bQanNdZskTAs6bg9h3ePKnRFd DYgLwVCqbqf6S4eifJ6UT8kjDItPayPnCCX6PPdI5AdvK5wAyh6oOld5Wwz17pf6CwsrBNdl y7br9ooqFajwLDnIt9PXx9HqzINj4WO7x0K0UTx85BBXTPb5ktI4znMTRsNoNRhB5vkvKUCk rDy
- Ironport-sdr: 641c87e1_yKRTYkEjgibOkcKK5Kay/oy/gcrzSZF5MS7nAaGM8QR7WFp 16snoEd5NLvPOFh7PywH++nJGIpcRWwrbKL8l9A==
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 thewhitespace 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?-- Abhishekhttp://www.cs.cornell.edu/~aa755/
- [Coq-Club] correct offsets in .glob files when unicode characters are present, Abhishek Anand, 03/23/2023
- Re: [Coq-Club] correct offsets in .glob files when unicode characters are present, Jim Fehrle, 03/23/2023
- Re: [Coq-Club] correct offsets in .glob files when unicode characters are present, Abhishek Anand, 03/23/2023
- Re: [Coq-Club] correct offsets in .glob files when unicode characters are present, Abhishek Anand, 03/23/2023
- Re: [Coq-Club] correct offsets in .glob files when unicode characters are present, Abhishek Anand, 03/23/2023
- Re: [Coq-Club] [Emacs] correct offsets in .glob files when unicode characters are present, Stefan Monnier, 03/23/2023
- Re: [Coq-Club] correct offsets in .glob files when unicode characters are present, Jim Fehrle, 03/23/2023
Archive powered by MHonArc 2.6.19+.