Unicode characters in CoCalc

Stream: general

[Vaibhav Karve]

I asked the same question on the #new members stream but didn't get an answer there, so I am asking it here.

How do I get all the unicode variants for notational symbols to show in Cocalc? For example, in Emacs when I type \r (in lean-mode) I get a whole variety of symbols that I can choose from by using the <right-arrow>/<left-arrow>. How do I get these options when writing code on cocalc? Is there some shortcut/trick for this?

[Bryan Gin-ge Chen]

You could try opening an issue at the cocalc github.

[Reid Barton]

trick = use emacs inside CoCalc? :upside_down:

[Vaibhav Karve]

Reid Barton said:

trick = use emacs inside CoCalc? :upside_down:

Wait, that's possible !?

[Johan Commelin]

Open a terminal, and type emacs

[Reid Barton]

I think so, you can just open a shell and run emacs inside it.

[Vaibhav Karve]

Oh. Haha. I assumed you meant I can get emacs-style editing in the regular Cocalc window.

[Reid Barton]

Right, that's why I didn't think it was a serious answer to your question.

[Vaibhav Karve]

Bryan Gin-ge Chen said:

You could try opening an issue at the cocalc github.

Thanks. I opened a support ticket.