Pause updating the goal buffer and leave it open?

Stream: Emacs

[Kent Van Vels]

Often times I want to write line (n+1) of a proof while looking at the goal window for line n. I usually just write my new line as a comment, so the current goal state doesn't change. However, I am wondering if there is a better way pause the LSP from updating the goal window. Is this possible? Thanks!

[Shanghe Chen]

Yeah pausing the updating for the goal buffer is nice. Maybe an alternative way is writing some function to automatically create a "snapshot" buffer for the goal buffer like

(defun xah-new-empty-buffer ()
  "Create a new empty buffer.
Returns the buffer object.
New buffer is named untitled, untitled<2>, etc.

Warning: new buffer is not prompted for save when killed, see `kill-buffer'.
Or manually `save-buffer'

URL `http://xahlee.info/emacs/emacs/emacs_new_empty_buffer.html'
Created: 2017-11-01
Version: 2022-04-05"
  (interactive)
  (let ((xbuf (generate-new-buffer "untitled")))
    (switch-to-buffer xbuf)
    (funcall initial-major-mode)
    xbuf
    ))

? Here the snippet creating an untitled buffer. Some logic for automatically copying the goal buffer to it should be added though

[Mekeor Melire]

iiuc, this feature request is already formulated in this issue:
https://github.com/leanprover-community/lean4-mode/issues/22

and iiuc, the fork of ultronozom / @Paul Nelson provides this feature. see https://github.com/ultronozm/eldoc-icebox.el and https://github.com/ultronozm/czm-lean4.el and https://github.com/ultronozm/lean4-mode