search

m-fleury / isabelle-emacs

Clone of isabelle, with LSP extensions in seperate branches
Other
25 stars 5 forks source link

copy-paste from lsp-isar-state to the thy file goes crazy #6

Closed m-fleury closed 4 years ago

m-fleury commented 4 years ago

@gh-salt I am afraid this one is a crazy evil bug (I am starting to understand why it is called evil). When I copy-paste a formula from the lsp-isar-state buffer, e.g. “∀N. Red_Inf_Q N ⊆ Inf”, to the thy file I am working in, I get the following result “\ Red_Inf_Q N \ Infnf”. To be more accurate, I have the time to see the proper formula being pasted and a fraction of a second later, it gets iteratively replaced by the crazy one from left to right. Here is another nice one: ∀B N. B ∈ Bot ⟶ N ⊨Q {B} ⟶ N - Red_F_Q N ⊨Q {B}

turns into \<forall>N. B \<in><in> \<longrightarrow><longrightarrow><longrightarrow>{B}\<Turnstile>N - Re\<longrightarrow>_Q N \<Turnstile><Turnstile><Turnstile> N \<Turnstile>Q {B}>Q {B} {B}B} Note that this doesn’t happen when I copy-paste from the thy file to itself.

m-fleury commented 4 years ago

@m-fleury Oh boy. I will attempt to reproduce it this week-end.

‌Can you try the following thing:

  1. does it happen without quail?
  2. does it happen when paste via M-: (insert “text to insert”)?
m-fleury commented 4 years ago

@gh-salt

  1. Yes it still happens when I do the copy-paste after having called quail-deactivate.
    1. Also yes.
m-fleury commented 4 years ago

@gh-salt Note that I am not convinced quail-deactivate really worked because I still get symbols automatically replaced even though I didn’t reactivate it.

m-fleury commented 4 years ago

@gh-salt This appears to be a spacemacs only bug and it doesn’t occur on emacs 27 with the new jason parser. It seems connected to isabelle sending symbol replacements through lsp, for example “exists n iota” with exist and iota in UTF8 to “\ n \” goes wrong (and the behaviour changes if s or o replaces the n).