From 3cd381b0f79ddef61355c0aae5dcdd466a303747 Mon Sep 17 00:00:00 2001
From: Soonho Kong <soonhok@cs.cmu.edu>
Date: Wed, 13 Aug 2014 15:05:46 -0700
Subject: [PATCH] fix(emacs): remove lean-get-this-if-true-or-that

---
 src/emacs/lean-mode.el | 7 +++----
 src/emacs/lean-util.el | 7 +------
 2 files changed, 4 insertions(+), 10 deletions(-)

diff --git a/src/emacs/lean-mode.el b/src/emacs/lean-mode.el
index 494b328ce7..6b6d170ca6 100644
--- a/src/emacs/lean-mode.el
+++ b/src/emacs/lean-mode.el
@@ -25,12 +25,11 @@
   "Execute Lean in the current buffer"
   (interactive "sarg: ")
   (let ((target-file-name
-         (lean-get-this-if-true-or-that
-          (buffer-file-name)
-          (flymake-init-create-temp-buffer-copy 'lean-create-temp-in-system-tempdir))))
+         (or (buffer-file-name)
+             (flymake-init-create-temp-buffer-copy 'lean-create-temp-in-system-tempdir))))
     (compile (lean-compile-string
               (lean-get-executable lean-executable-name)
-              (lean-get-this-if-true-or-that arg "")
+              (or arg "")
               target-file-name))))
 
 (defun lean-std-exe ()
diff --git a/src/emacs/lean-util.el b/src/emacs/lean-util.el
index 54530d8006..cb187cf83c 100644
--- a/src/emacs/lean-util.el
+++ b/src/emacs/lean-util.el
@@ -4,13 +4,8 @@
 ;; Author: Soonho Kong
 ;;
 
-(defmacro lean-get-this-if-true-or-that (this that)
-  `(cond (,this ,this)
-         (t ,that)))
-
 (defun lean-get-rootdir ()
-  (lean-get-this-if-true-or-that
-   lean-rootdir
+  (or lean-rootdir
    (error "'lean-rootdir' is not defined. Please have\
 (customize-set-variable 'lean-rootdir \"~/work/lean\")\
 in your emacs configuration.\