0

lean-mode (available on MELPA) defines two kinds of comments:

-- like this

and

/- 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. -/

becomes

/- 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...?

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.