isar-mode disables unicode-tokens-mode

[simonpannek]

Whenever I open a new file and use the auto-completion for unicode symbols, the auto-completion extends to the actual unicode symbol instead of using the isabelle style (for example ⊆ instead of \). For a friend of mine, this seems to be fixed by toggling unicode-tokens-mode off and on again. This doesn't work for me and instead, disables isar-mode completely. This means after trying to toggle the tokens mode, the whole file is not displayed in the Isabelle style anymore. Do you have any idea how I could fix this? Thanks!

[m-fleury]

It is very tough for me to debug this without being able to reproduce it. Can you send me your config (or enough of your config to reproduce the problem) + your emacs version?

(Either posting it here if you are comfortable with it or sending it per email).

[simonpannek]

Hi, thanks for the quick response! Sure, this should be enough of my config to reproduce the problem:

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

(use-package! isar-mode
  :mode "\\.thy\\'"
  :config
  ;; (add-hook 'isar-mode-hook 'turn-on-highlight-indentation-mode)
  ;; (add-hook 'isar-mode-hook 'flycheck-mode)
  (add-hook 'isar-mode-hook 'company-mode)
  (add-hook 'isar-mode-hook
            (lambda ()
              (set (make-local-variable 'company-backends)
                   '((company-dabbrev-code company-yasnippet)))))
  (add-hook 'isar-mode-hook
            (lambda ()
              (set (make-local-variable 'indent-tabs-mode) nil)))
  (add-hook 'isar-mode-hook
            (lambda ()
              (yas-minor-mode)))
  )

(use-package! lsp-isar-parse-args
  :custom
  (lsp-isar-parse-args-nollvm nil))

(use-package! lsp-isar
  :commands lsp-isar-define-client-and-start
  :custom
  (lsp-isar-output-use-async t)
  (lsp-isar-output-time-before-printing-goal nil)
  (lsp-isar-experimental t)
  (lsp-isar-split-pattern 'lsp-isar-split-pattern-two-columns)
  (lsp-isar-decorations-delayed-printing t)
  :init
  (add-hook 'lsp-isar-init-hook 'lsp-isar-open-output-and-progress-right-spacemacs)
  (add-hook 'isar-mode-hook #'lsp-isar-define-client-and-start)

  (push (concat "~/Library/isabelle-emacs/src/Tools/emacs-lsp/yasnippet")
   yas-snippet-dirs)
  (setq lsp-isar-path-to-isabelle "~/Library/isabelle-emacs")
  )

;; https://github.com/m-fleury/isabelle-release/issues/21
(defun ~/evil-motion-range--wrapper (fn &rest args)
  "Like `evil-motion-range', but override field-beginning for performance.
     See URL `https://github.com/ProofGeneral/PG/issues/427'."
          (cl-letf (((symbol-function 'field-beginning)
                                  (lambda (&rest args) 1)))
                       (apply fn args)))

            (advice-add #'evil-motion-range :around #'~/evil-motion-range--wrapper)

(map! :leader :map 'isar-mode-map :localleader
      (:prefix ("t" . "Try0...")
                :desc "Insert try0"           "t" #'lsp-isar-insert-try0
                :desc "Insert proof"          "p" #'lsp-isar-insert-try0-proof)
      (:prefix ("s" . "Sledgehammer...")
                :desc "Open interface"        "s" #'lsp-isar-sledgehammer-interface
                :desc "Insert with interface" "S" #'lsp-isar-insert-sledgehammer-and-call
                :desc "Insert sledgehammer"   "i" #'lsp-isar-insert-sledgehammer)
        :desc "Insert auto"          "a" #'lsp-isar-insert-auto
        :desc "Insert simp"          "b" #'lsp-isar-insert-simp
        :desc "Insert meson"         "e" #'lsp-isar-insert-meson
        :desc "Insert fastforce"     "f" #'lsp-isar-insert-fastforce
        :desc "Insert algebra"       "g" #'lsp-isar-insert-algebra
        :desc "Insert linarith"      "l" #'lsp-isar-insert-linarith
        :desc "Insert force"         "F" #'lsp-isar-insert-force
        :desc "Insert fast"          "o" #'lsp-isar-insert-fast
        :desc "Insert presburger"    "p" #'lsp-isar-insert-presburger
        :desc "Insert argo"          "r" #'lsp-isar-insert-argo
        :desc "Insert satx"          "x" #'lsp-isar-insert-satx
        :desc "Insert proof outline" "P" #'lsp-isar-insert-proof-outline
        :desc "Delete windows"       "K" #'delete-other-windows) ;; not quite finished

;; Semantic syntax highlighting
(add-hook 'lsp-mode-hook 'lsp-semantic-tokens-mode)

;; Treemacs keybindings
(map! :leader :map 'treemacs-mode-map :localleader
      :desc "Switch workspace" "s" #'treemacs-switch-workspace
      :desc "Edit workspaces"  "e" #'treemacs-edit-workspaces
      :desc "Add project"      "a" #'treemacs-add-project-to-workspace
      :desc "Remove project"   "R" #'treemacs-remove-project-from-workspace
      :desc "Rename project"   "r" #'treemacs-rename-project)

;; Fix backslash
(defun insert-backslash ()
  (interactive)
  (insert "\\"))

(global-unset-key (kbd "M-/"))
(map! "M-/" #'insert-backslash)

and here you can find my emacs version:

GNU Emacs     v28.2            nil
Doom core     v3.0.0-pre       HEAD -> master d5ccac5d7 2022-12-02 00:36:06 +0100
Doom modules  v22.10.0-pre     HEAD -> master d5ccac5d7 2022-12-02 00:36:06 +0100

Thanks for looking into this, please let me know if you need anything else.

[m-fleury]

Okay this is weird: If I take your config as is, replacing only the path in lsp-isar-path-to-isabelle, it works

Is there anything in your *messages* buffer?

[simonpannek]

Okay, that's very weird. Maybe it's something OS related (I'm on a M1 Mac). Here is the complete *Messages* buffer while the problem occured:

Doom loaded 233 packages across 43 modules in 1.328s
Package cl is deprecated [2 times]
[Treemacs] Selected workspace semantics.
Loading /Users/simonpannek/.emacs.d/.local/cache/recentf...done
[yas] Check your `yas-snippet-dirs': /Users/simonpannek/.doom.d/snippets/ is not a directory
[yas] Prepared just-in-time loading of snippets with some errors.  Check *Messages*.
Waiting for git... [2 times]
don’t debug indentation
installing config (tramp: No)
LSP :: Connected to [lsp-isar:48965/starting].
Note: standard-indent, tab-width, evil-shift-width adjusted to 2
Making maths-menu-filter-predicate buffer-local while locally let-bound!
Making maths-menu-tokenise-insert buffer-local while locally let-bound!
Making maths-menu-filter-predicate buffer-local while locally let-bound!
Making maths-menu-tokenise-insert buffer-local while locally let-bound!
LSP :: lsp-isar:48965 initialized successfully in folders: (/Users/simonpannek/path/to/project)
LSP :: Welcome to Isabelle/HOL (Isabelle2022-vsce)

I added a snippets folder to my doom.d folder to get rid of the yas error message, but that didn't fix it either :/

[m-fleury]

Mhhh does reactivating prettify-symbols-mode bring back the symbols?

[simonpannek]

Yes, but it does not fix the issue where the symbols are not getting replaced with the isabelle style tokens.

[m-fleury]

Sorry for the very late answer, I took two weeks off the computer over Christmas.

I did randomly see a similar issue (but could not reproduce it...). Reactivating the symbols was not sufficient to trigger a reprinting of the screen, but every new typed was properly replaced by isabelle style tokens (and when changing a line, the symbols of the line were also replaced).

I guess that this does not work for you either?

[simonpannek]

All good, took some time off as well :)

Yes, this also happens for me, but only if I run ~/isar-fix-unicode...

[m-fleury]

There are two toggles:

• unicode-symbols-mode is responsible for the symbol completion (aka replacing ==> by \<Longrightarrow>)
• prettify-symbols-mode is responsible for prettifyng the symbols (aka replacing \` by the proper arrow)

If you remove ~/isar-fix-unicode which of those two do you need to run to get everything running?

[simonpannek]

Hi,

sorry for the late response. With one of the recent updates (I think it was a doom update), this issue seems to be solved now. If this ends up happening again, I can reopen this issue if you want me to. Thanks!

[gh-salt]

It appears the proposed fix is not always sufficient.