Initially, I thought that #74 was reporting this issue, but it seems I kind of misread it and it actually does not!
I've had an issue (specific to Doom Emacs) where the unicode tokens mode does not get fully activated (in fact, only the quail input method is not set up; there is no u in the modeline nor is ==> translated to \<Longrightarrow>) only for files which are not opened first.
So let's say I have three files A.thy, B.thy and C.thy. Opening A.thy works correctly, and the input method is set up. But then, opening B.thy (through :edit B.thy) does not work correctly, although the isar mode is correctly set up (just not the input method).
I have tried to set the input method manually to Unicode tokens after opening the file, but it seems to have no effect (or at least, the input method is not activated). Providing a hook to isar-mode-hook which does just that ((set-input-method "Unicode tokens")) also has no effect.
Adding the comment(* -*- eval: (set-input-method "Unicode tokens") -*- *) at the top of the file seems to fix the problem, but this is not a viable solution (generally speaking, using eval in this way is unsafe).
I have also found that trying to debug calls to unicode-tokens-mode (using edebug-eval-top-level-form) also fixes the issue, somehow! Perhaps it allows to wait for a very small amount of time at the correct moment?
My best guess would be a timing issue somewhere in the code (which only affects Doom Emacs as far as I tested?), although inserting e.g. (sleep-for 1) before (set-input-method "Unicode tokens") in unicode-tokens-mode does not fix the issue.
Initially, I thought that #74 was reporting this issue, but it seems I kind of misread it and it actually does not! I've had an issue (specific to Doom Emacs) where the unicode tokens mode does not get fully activated (in fact, only the quail input method is not set up; there is no
uin the modeline nor is==>translated to\<Longrightarrow>) only for files which are not opened first. So let's say I have three filesA.thy,B.thyandC.thy. OpeningA.thyworks correctly, and the input method is set up. But then, openingB.thy(through:edit B.thy) does not work correctly, although the isar mode is correctly set up (just not the input method).I have tried to set the input method manually to
Unicode tokensafter opening the file, but it seems to have no effect (or at least, the input method is not activated). Providing a hook toisar-mode-hookwhich does just that ((set-input-method "Unicode tokens")) also has no effect.Adding the comment
(* -*- eval: (set-input-method "Unicode tokens") -*- *)at the top of the file seems to fix the problem, but this is not a viable solution (generally speaking, usingevalin this way is unsafe). I have also found that trying to debug calls tounicode-tokens-mode(usingedebug-eval-top-level-form) also fixes the issue, somehow! Perhaps it allows to wait for a very small amount of time at the correct moment?My best guess would be a timing issue somewhere in the code (which only affects Doom Emacs as far as I tested?), although inserting e.g.
(sleep-for 1)before(set-input-method "Unicode tokens")inunicode-tokens-modedoes not fix the issue.