lean-mode (available on MELPA) defines two kinds of comments:
-- like this
/- like this -/
I've noticed that when filling long lines, the behavior is sometimes not optimal. E.g.,
/- xxx xxxx xx.xxxxx xx xxxx xx xxxxxx xxx xxxxxxxxx xxxxxxxxx xxxxx, xxxxx xxxxx xxx xxxx xxxxxxxx xxxxxxxxxxxxx. -/
/- xxx xxxx xx.xxxxx xx xxxx xx xxxxxx xxx xxxxxxxxx xxxxxxxxx xxxxx, /- xxxxx xxxxx xxx xxxx xxxxxxxx xxxxxxxxxxxxx. -/
This is actually an error in Lean ("unexpected end of comment block").
I looked at the syntax defined for the two types of comments and it seems correct:
(modify-syntax-entry ?/ ". 14nb" st) (modify-syntax-entry ?- ". 123" st)
I tried defining and setting my own
adaptive-fill-function. It runs (according to
edebug-defun) and the
cond branches are entered appropriately, but it doesn't seem to have an effect on the comment-filling behavior.
(defun lean-fill-function () (cond ((looking-at "/-") " ") ((looking-at "--") "-- ") (t nil))) (setq adaptive-fill-function 'lean-fill-function)
Can someone explain how to fill long block comments without inserting
/- as a prefix?
Note that C mode has similar block comments (
/* like this */) and uses an elaborate custom fill function that works. One thought would be to advise Lean mode to use a variant of the c-mode functions...?