An Emacs snippet for ACL2 certification in shell buffers

acl2-cert-dimmer-for-comint.el

  ;; 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)