coq-debug-eauto.el

(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!")))