emacs users

Stream: general

[Simon Hudon]

Hello fellow emacs user(s)! I have just put a package yasnippet-lean up on melpa. Feel free to contribute other snippets if I missed any. https://github.com/leanprover-community/yasnippet-lean

[Jesse Michael Han]

we added some more features! a GIF is worth a thousand words: yasnippet-lean-test.gif

[Mario Carneiro]

The suffices formatting doesn't make sense for tactic mode

[Mario Carneiro]

not sure whether you can do something about this without lean server giving you more info

[Jesse Michael Han]

i think snippets can execute arbitrary elisp so it might be possible to accommodate that

[Jesse Michael Han]

i think the only indicator of whether or not you're in tactic mode is that the replies to info requests include a formatted tactic_state iff you're in tactic mode... so it might be a bit of a hack to implement

[Gun Pinyo]

I am having a problem with expand-region and lean-mode
basically if I have "abc.def_gh" and put the cursor at "e", expand the region once we should get "def" then "def_gh" then "abc.def_gh" however, in my case, it goes from "e" to "abc.def_gh" directly. This is very wired since lisp-mode and text-mode agree on the correct behaviour.

Is there anyone has the same problem?

[Kevin Buzzard]

Hardly anyone here uses emacs for Lean (which is funny in my case because I use it for everything else). We could try pinging @Reid Barton

[Patrick Massot]

Sebastian also uses it

[Sebastian Ullrich]

Unfortunately I don't use expand-region

[Kevin Buzzard]

...because you broke it? :P

[Yury G. Kudryashov]

I use Lean with Emacs but don't use expand-region

[Yury G. Kudryashov]

I can try it tomorrow

[Jesse Michael Han]

I am having a problem with expand-region and lean-mode
basically if I have "abc.def_gh" and put the cursor at "e", expand the region once we should get "def" then "def_gh" then "abc.def_gh" however, in my case, it goes from "e" to "abc.def_gh" directly. This is very wired since lisp-mode and text-mode agree on the correct behaviour.

Is there anyone has the same problem?

this might be because there expand-region has mode-specific expansions for lisp-mode and text-mode which aren't enabled in a lean-mode buffer. you might be able to get away with copying whatever configuration is there for lisp-mode and changing lisp-mode to lean-mode

[Gun Pinyo]

I am having a problem with expand-region and lean-mode
basically if I have "abc.def_gh" and put the cursor at "e", expand the region once we should get "def" then "def_gh" then "abc.def_gh" however, in my case, it goes from "e" to "abc.def_gh" directly. This is very wired since lisp-mode and text-mode agree on the correct behaviour.

Is there anyone has the same problem?

this might be because there expand-region has mode-specific expansions for lisp-mode and text-mode which aren't enabled in a lean-mode buffer. you might be able to get away with copying whatever configuration is there for lisp-mode and changing lisp-mode to lean-mode

I have searched the entire expand-region repository but it doesn't mention lisp-mode at all. The functionality is there by default. Even I state explicitly, it doesn't work.

[Jesse Michael Han]

that's odd, maybe expand-region queries something else which does change depending on the current mode

[Jesse Michael Han]

for the convenience of other emacs users of lean-mode, i've made a gist available with my lean-mode customizations here

[Alexandre Rademaker]

It is annoying that if you use C-c C-b to see message boxes, if a command is followed by a comment, the message is inserted after it

[Reid Barton]

You can work around this by ending the command with a .