Skip to content

Instantly share code, notes, and snippets.

@kini
Last active May 23, 2018 17:24
Show Gist options
  • Save kini/c00bd6d1916da1234ff066648971befd to your computer and use it in GitHub Desktop.
Save kini/c00bd6d1916da1234ff066648971befd to your computer and use it in GitHub Desktop.
An Emacs snippet for ACL2 certification in shell buffers
;; ACL2 certification dimmer function
(defun acl2-cert-dimmer-for-comint (str)
"When cert.pl says it has certified something, go back and
dim the text where it said it was making that thing. This way
you can easily tell at a glance what books are still certifying."
(let ((pos-in-str nil)
;; This is broken; comint-last-input-end isn't really the
;; end of the last input. I should probably search to the
;; previous prompt, or something.
(beginning-of-output comint-last-input-end))
;; dim the "Making ..." lines
(while (setq pos-in-str
(string-match "^Built \\(.*\\.cert\\)"
str pos-in-str))
(incf pos-in-str)
(let ((filename (match-string-no-properties 1 str)))
(save-excursion
(search-backward (concat "Making " filename)
beginning-of-output)
(add-text-properties (line-beginning-position)
(line-end-position)
'(font-lock-face shadow)))))))
(add-hook 'comint-output-filter-functions
#'acl2-cert-dimmer-for-comint)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment