How to expand emacs's eldoc's echo area?

Stream: new members

[Kritixi Lithos]

I'm using lean-mode on emacs 27.1 for lean3. When my cursor is over the name of, say, a tactic, the echo area displays a description of the tactic. For example, for simp I see The simp tactic uses lemmas and hypotheses to simplify the main goal target or non-dependent hypotheses. It has many variants. …. Particularly, it finishes with an ellipsis. How do I expand this? (setq eldoc-echo-area-use-multiline-p t) doesn't change anything. I realise that the full tactic reference is also available here https://leanprover.github.io/reference/tactics.html , but how do I see this in emacs?

[Yury G. Kudryashov]

I don't understand what in lean-eldoc-documentation-function truncates the message.

[Yury G. Kudryashov]

It's in lean-info-record-to-string

[Yury G. Kudryashov]

        (let* ((lines (split-string doc "\n"))
               (doc (if (cdr lines)
                        (concat (car lines) " ⋯")
                      (car lines))))
          (setq str (concat str
                            (format "\n%s"
                                    (propertize doc 'face 'font-lock-comment-face))))))

[Yury G. Kudryashov]

This code should be fixed to use eldoc-echo-area-use-multiline-p

[Kritixi Lithos]

Yury G. Kudryashov said:

It's in lean-info-record-to-string

Thanks, I'll mess around with this, and see if I succeed with a pull request

[Kritixi Lithos]

BTW I've chosen instead to port to emacs 28, and have created https://github.com/leanprover/lean-mode/issues/33 regarding this