Bringing back (* Coq style *) comments

[catalin-hritcu]

Is there any way I can get back ( Coq style ) comments? I often use comment-region / uncomment-region and for that I find Coq style comments to be much superior to the current // comments. In particular, the regions I want to comment out and back in are often only part of a line or start with part of a line, in which case Coq style comments can be added in and removed without destroying the existing line structure and indentation of the code.

[cpitclaudel]

This should do it:

(add-hook 'fstar-mode-hook
          (lambda () (setq-local comment-start "(* "
                                 comment-continue ""
                                 comment-end " *)")))

Want a setting?

[catalin-hritcu]

If it worked this would be good enough for me. It gives the following error though:

Eager macro-expansion failure: (wrong-number-of-arguments (2 . 2) 6)

And an option would probably be nice in general :)

[cpitclaudel]

Surprising error. Can you show a backtrace?

[catalin-hritcu]

Surprising error. Can you show a backtrace?

What should I do to get one? :)

[cpitclaudel]

If it happens at startup, you can start emacs with --debug-init (emacs --debug-init). If it happens during normal operation, you can run M-x toggle-debug-on-error before reproducing the issue.

[catalin-hritcu]

None of these seems to have any effect. I added the snippet above to .emacs and get the error in the *Messages* window at startup or if I eval-region this snippet, but nothing changes if debugging is enabled.

[cpitclaudel]

Oh, I think I know what's happening. Try this:

(add-hook 'fstar-mode-hook
          (lambda ()
            (setq-local comment-start "(* ")
            (setq-local comment-continue "")
            (setq-local comment-end " *)")))

[catalin-hritcu]

This works. Thanks a lot.