Skip to content

Instantly share code, notes, and snippets.

@HuStmpHrrr
Last active July 24, 2018 03:45
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
Star You must be signed in to star a gist
Save HuStmpHrrr/ea412d37e7718d42d4a6e46097c66f8b to your computer and use it in GitHub Desktop.
(defun coq-debug-eauto-output--transform (flag)
(goto-char (line-beginning-position))
(let ((line (buffer-substring-no-properties
(line-beginning-position)
(line-end-position))))
(pcase line
("" nil)
("Debug: (* debug eauto: *)"
(delete-region (line-beginning-position) (line-end-position))
(if flag (insert "}\n"))
(insert "{")
t)
(_
(if (re-search-forward "\\(.*?depth=[[:digit:]]+\\)[[:space:]]+\\(.*\\)"
(line-end-position)
t)
(replace-match " (* \\1 *) \\2.")
(insert " (* ")
(goto-char (line-end-position))
(insert " *)"))
nil))))
(defun coq-debug-eauto-output-proc (arg)
"transform `debug eauto' into runnable output.
put prefix key if one wants to yank it immediately."
(interactive "P")
(if proof-response-buffer
(progn
(with-temp-buffer
(let ((tmp (current-buffer))
(open nil))
(with-current-buffer proof-response-buffer
(copy-to-buffer tmp 1 (point-max)))
(goto-char 1)
(while (not (= (point) (point-max)))
(setq open (or (coq-debug-eauto-output--transform open)
open))
(forward-line 1))
(if open (insert "}"))
(copy-region-as-kill 1 (point-max))))
(if arg (yank)))
(error "there is no proof general response buffer!")))
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment