unicode autoinsertion changes

[halbGefressen]

When I type => on my old machine, it automatically converts it to \<Rightarrow> (desired behaviour). Apparently something has changed in yasnippet, so now with the exact same configuration on my other machine where I upgraded a couple of packages (including yasnippet, which does the completion apparently) it doesn't automatically convert it anymore. I now have to press tab to convert => to \<Rightarrow> (and similar symbols).

I'm on the Isabelle2021-1-more-vscode branch on both machines. Some questions: What is the module/package that provides the desired functionality? Maybe I can fix it myself.

[m-fleury]

quail is doing the symbol replacement, not yasnippet.

[m-fleury]

The minor mode is called: unicode-tokens-mode. Can you check with describe-mode that it is activated?

[halbGefressen]

Yes, it is enabled and the completion still doesn't work right after opening a .thy file. However, after manually disabling and re-enabling it, the completion suddenly starts working.

[halbGefressen]

ugly workaround that seems to fix it on my machine:

(defun ~/isar-fix-unicode ()
  (interactive) (unicode-tokens-mode) (unicode-tokens-mode))

then add it as an isar-mode-hook

[m-fleury]

That seems to indicate an error. Can you eval M-x toogle-debug-on-error before running unicode-tokens-mode (for example, by first evaluating then only opening the file)? This should give an backtrace of the problem…

The issue does not come from isabelle but from the isar-mode, so you don't have to wait until isabelle starts each time…

Which emacs version are you using?

[halbGefressen]

I did, where can I find the backtrace? I'm using emacs-nativecomp-28.2-1 from arch-extra in combination with the latest doom emacs revision.

[halbGefressen]

*Messages*:

Debug on Error enabled globally
Loading /home/christian/.emacs.d/.local/cache/recentf...done
don’t debug indentation
installing config (tramp: No)
Submission.thy is not part of any project.

i ==> Import project root /home/christian/Uni/Übungen/Sem5/Semantik/ha4/Semantics_2021/2022-Homework_4/
I ==> Import project by selecting root directory interactively
. ==> Import project at current directory /home/christian/Uni/Übungen/Sem5/Semantik/ha4/Semantics_2021/2022-Homework_4/
d ==> Do not ask again for the current project by adding /home/christian/Uni/Übungen/Sem5/Semantik/ha4/Semantics_2021/2022-Homework_4/ to lsp-session-folders-blacklist
D ==> Do not ask again for the current project by selecting ignore path interactively
n ==> Do nothing: ask again when opening other files from the current project

Select action: i
LSP :: Guessed project root is ~/Uni/Übungen/Sem5/Semantik/ha4/Semantics_2021/2022-Homework_4
LSP :: Connected to [lsp-isar:6475/starting].
Note: standard-indent, tab-width, evil-shift-width adjusted to 2
LSP :: Welcome to Isabelle/HOL (repository version)
LSP :: lsp-isar:6475 initialized successfully in folders: (/home/christian/Uni/Übungen/Sem5/Semantik/ha4/Semantics_2021/2022-Homework_4)

*lsp-log*:

Command "~/Programme/isabelle-emacs/bin/isabelle vscode_server -o vscode_unicode_symbols -o vscode_pide_extensions -o vscode_caret_perspective=10 -m do_notation" is present on the path.
Command "~/Programme/isabelle-emacs/bin/isabelle vscode_server -o vscode_unicode_symbols -o vscode_pide_extensions -o vscode_caret_perspective=10 -m do_notation" is present on the path.
Found the following clients for /home/christian/Uni/Übungen/Sem5/Semantik/ha4/Semantics_2021/2022-Homework_4/Submission.thy: (server-id lsp-isar, priority 1)
The following clients were selected based on priority: (server-id lsp-isar, priority 1)
Unofficial version of Isabelle/HOL (repository version)

[m-fleury]

The good news: I can reproduce the issue in doom. The bad news: I have yet to investigate it…

[halbGefressen]

For now, the fix works fine and has no disadvantages afaik. I'll try to debug as well (with my yet very limited skillset, so don't expect much :P).

[m-fleury]

Okay, I am at a loss what is happening here. It seems that unicode-tokens-mode is starting too fast and delaying it ensures that the initialization is done properly.

On my machine I have swapped two instructions (https://github.com/m-fleury/isar-mode/commit/8675631462517a0a2723405177ef86d06dfaa6d5) and it works now on my machine. Somehow.

That is why I love-hate emacs: debugging is so random…

[m-fleury]

Marking as solved (most likely). Reopen if not.