Stream: VsCoq devs & users

Topic: Prettify completely broken?


view this post on Zulip 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...

view this post on Zulip Yannick Zakowski (May 14 2021 at 09:20):

Is the issue known, or am I missing something?

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Théo Winterhalter (May 14 2021 at 10:36):

Yes… Anyway, I assume the issue is from the Prettify symbol side, isn't it?

view this post on Zulip Théo Winterhalter (May 14 2021 at 10:37):

If you require import Utf8 you still get things like , λ, and .

view this post on Zulip 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 :)

view this post on Zulip Yannick Zakowski (May 15 2021 at 09:11):

I opened an issue on the Github to raise the question.


Last updated: Jan 30 2023 at 18:04 UTC