     (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))
+          (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"))))
 
 
-
-;; ###autoload
-(define-derived-mode redprl-mode prog-mode "RedPRL" "Major mode for editing RedPRL proofs."
-
-  (set (make-variable-buffer-local 'comment-start) "// ")
+(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)))
+       `(("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)

;; Copyright (C) 2016  Jonathan Sterling

;; Author: Jonathan Sterling <jon@jonmsterling.com>
;; Keywords: languages

;; This program is free software; you can redistribute it and/or modify


;;; Commentary:

;; This is a major mode for editing RedPRL developments.  The current
;; editing features include simple syntax highlighting, imenu, and
;; completion support.  Additionally, there is a command to run RedPRL
;; in a compilation buffer.
;;
;; RedPRL can be obtained from https://github.com/RedPRL/sml-redprl .
;;
;; Make sure to set the variable `redprl-command' to the location of the
;; redprl binary.

;;; Code:

