 
 (defface redprl-sort-face
   '((t (:inherit font-lock-type-face))) "Face for RedPRL's built-in sorts."
+  :group 'redprl)
+
+(defface redprl-atom-face
+  '((t (:inherit font-lock-constant-face))) "Face for RedPRL's atoms."
   :group 'redprl)
 
 (defcustom redprl-command "redprl"


;;; Commentary:

;;

;;; Code:


    (if filename
        (progn
          (when (buffer-modified-p) (save-buffer))
          (let* ((dir (file-name-directory filename))
                 (file (file-name-nondirectory filename))
                 (command (concat redprl-command " " file))

                 ;; Emacs compile config stuff - these are special vars
                 (compilation-buffer-name-function
                  'redprl--compilation-buffer-name-function)
                 (default-directory dir))
            (compile command)))
      (error "Buffer has no file name"))))


(defconst redprl--revolutionary-sayings
  '("Decisively Smash the Formalist Clique!"
    "Long Live the Anti-Realist Struggle!"
    "We Can Prove It!")
  "Words of encouragement to be displayed when RedPRL is initially launched.")

(defun redprl-display-revolutionary-saying ()
  "Display a revolutionary saying to hearten RedPRL users."
  (interactive)
  (let ((revolutionary-saying (nth (random (length redprl--revolutionary-sayings))
                                   redprl--revolutionary-sayings)))
    (message "%s" revolutionary-saying)))

;;;###autoload
(define-derived-mode redprl-mode prog-mode "RedPRL"
  "Major mode for editing RedPRL proofs.
\\{redprl-mode-map}"

  (set (make-local-variable 'comment-start) "// ")
  
  (setq font-lock-defaults '((redprl-mode-font-lock-keywords) nil nil))

  (set (make-local-variable 'imenu-generic-expression)
       `(("Def" ,(rx-to-string redprl-def-name-regexp) 1)
         ("Thm" ,(rx-to-string redprl-thm-name-regexp) 1)
         ("Tac" ,(rx-to-string redprl-tac-name-regexp) 1)
         ("Sym" ,(rx-to-string redprl-sym-name-regexp) 1)
         ("Record" ,(rx-to-string redprl-record-name-regexp) 1)))

  ;; Bind mode-specific commands to keys
  (define-key redprl-mode-map (kbd "C-c C-l") 'redprl-compile-buffer)
