Zulip Chat Archive

Stream: general

Topic: Unicode characters in CoCalc


Vaibhav Karve (Jun 03 2020 at 18:24):

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 (Jun 03 2020 at 18:25):

You could try opening an issue at the cocalc github.

Reid Barton (Jun 03 2020 at 18:26):

trick = use emacs inside CoCalc? :upside_down:

Vaibhav Karve (Jun 03 2020 at 18:27):

Reid Barton said:

trick = use emacs inside CoCalc? :upside_down:

Wait, that's possible !?

Johan Commelin (Jun 03 2020 at 18:27):

Open a terminal, and type emacs

Reid Barton (Jun 03 2020 at 18:27):

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

Vaibhav Karve (Jun 03 2020 at 18:28):

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

Reid Barton (Jun 03 2020 at 18:30):

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

Vaibhav Karve (Jun 03 2020 at 18:42):

Bryan Gin-ge Chen said:

You could try opening an issue at the cocalc github.

Thanks. I opened a support ticket.


Last updated: Dec 20 2023 at 11:08 UTC