invisible artefacts from Alt-/ autocompletion polluting the file

[m-fleury]

@gh-salt Several times I have weird syntax errors and when I type the same thing again they work. It is hard to isolate the bug cleanly because when it happens, I am not sure if I really have made a syntax error or if this bug is triggered, but I currently have an example where it is clear that I am not responsible . Here is what is in my .thy file:

unfolding consequence_relation_def
proof (intro conjI)
show \<open>Bot \<noteq> {}\<close> using Bot_not_empty
qed```

and here is the error message I get in lsp-isar-output:

Undefined fact: "Bot_not_emptyshow"⌂

My guess is that this happens when I use the completion with Alt-/. For example, I can produce a similar bug by typing lemma followed by Alt-/ (which adds the cartouche) and then after completing the lemma, e.g. `lemma \<open>True\<close>` by simp I get the following error output: Undefined method: "simplemma"⌂ . Note that it is not always this error that is triggered. For example, if I had a space after the simp then the error turns to Inner syntax error: unexpected end of input
Failed to parse prop. I hope this is not another weirdo spacemacs-related bug…

[m-fleury]

@m-fleury

I hope this is not another weirdo spacemacs-related bug… That’s look like post-self-insert-hook is not fired in that case and this definitely one of the things evil-mode changes.

I will need the output of (in an Isabelle buffer): M-: (message “%s” post-command-hook) M-: (message “%s” post-self-insert-hook)

If you can reproduce it consistently, evaluate:

(add-hook 'post-self-insert-hook (lambda () (message “I am here”))

and see if the message is printed after failed M-/ completion.

If the theory is right, this could solve it, but I am not certain:

(add-hook 'yas-after-exit-snippet-hook #'lsp--on-self-insert nil t)

[m-fleury]

@gh-salt M-: (message “%s” post-command-hook) "(evil-normal-post-command lsp-isar-update-caret lsp--highlight eldoc-schedule-timer yas--post-command-handler company-post-command flycheck-hide-error-buffer flycheck-display-error-at-point-soon flycheck-error-list-highlight-errors flycheck-error-list-update-source flycheck-perform-deferred-syntax-check lsp-ui-doc--make-request lsp-ui-sideline t)"

M-: (message “%s” post-self-insert-hook) "(sp--post-self-insert-hook-handler helm-find-files--reset-level-tree electric-indent-post-self-insert-function blink-paren-post-self-insert-function)" I reproduced the bug after having evaluated (add-hook 'post-self-insert-hook (lambda () (message “I am here”)) but “I am here” was never printed in the Message buffer (I tried several “successful” and really failed completions).

[m-fleury]

@m-fleury

I reproduced the bug after having evaluated (add-hook 'post-self-insert-hook (lambda () (message “I am here”)) but “I am here” was never printed in the Message buffer (I tried several “successful” and really failed completions). The message never stays long enough in the minibuffer to be visible, but you can see it in the Message buffer. (Sorry, I should have checked if it works).

[m-fleury]

@gh-salt Indeed, I was talking about the Message buffer all along.

[m-fleury]

@m-fleury Okay post-self-insert-hook is already strange (it is clearly missing one lsp-function).

How about

M-: (message "%s"after-change-function) ?

[m-fleury]

@gh-salt This is the output for M-: (message ”%s” after-change-function) Symbol’s value as variable is void: after-change-function

[m-fleury]

I believe this is another instance of #6.