Yannick Zakowski (May 14 2021 at 09:19): Yannick Zakowski (May 14 2021 at 09:19):I am using the "Prettify Symbol Mode" extension and am getting wild behaviors: it overall works, but sometimes suddenly introduce symbols seemingly randomly, and I can't find how to fix it without closing the file.
I am for instance right now staring at a line devoid of any character, but displaying λ⇒≜←←, a "Lemma" displayed as the three dots of "Proof", the sequence of character "triv" in the middle of the name of a lemma displayed as "∀", among others...
Yannick Zakowski (May 14 2021 at 09:20):Is the issue known, or am I missing something?
Théo Winterhalter (May 14 2021 at 10:08):I think I tried it when first trying vscoq, but it certainly wasn't as good as company-coq. Since then I decided that writing things in unicode from the start is probably the better approach.
Yannick Zakowski (May 14 2021 at 10:34):I don't disagree, but the primitives of the language and the standard library have not made this choice unfortunately
Théo Winterhalter (May 14 2021 at 10:36):Yes… Anyway, I assume the issue is from the Prettify symbol side, isn't it?
Théo Winterhalter (May 14 2021 at 10:37):If you require import Utf8 you still get things like ∀, λ, and ∧.
Yannick Zakowski (May 14 2021 at 10:40):Oh I actually didn't know of this module, thanks!
I'd still enjoy some prettification in the style of company-coq if that were possible I must say, but that's good to know :)
Yannick Zakowski (May 15 2021 at 09:11):I opened an issue on the Github to raise the question.
Last updated: Jun 04 2023 at 23:30 UTC