From 0fed6129dfe805942c8b618b82b56712e70d9630 Mon Sep 17 00:00:00 2001
From: Soonho Kong <soonhok@cs.cmu.edu>
Date: Tue, 28 Jul 2015 14:16:13 -0700
Subject: [PATCH] feat(emacs/lean-mode): add lean-show-goal-at-pos

which is bound to 'C-c C-g' by default. Depending on the current char,
it invokes lean-server with either '--goal' or '--hole' option.

close #749
---
 src/emacs/lean-mode.el | 23 ++++++++++++++++++-----
 src/emacs/lean-util.el |  5 +++++
 2 files changed, 23 insertions(+), 5 deletions(-)

diff --git a/src/emacs/lean-mode.el b/src/emacs/lean-mode.el
index 063f5700b..a177ce52e 100644
--- a/src/emacs/lean-mode.el
+++ b/src/emacs/lean-mode.el
@@ -145,6 +145,23 @@ will be flushed everytime it's executed."
     (set-process-coding-system p 'utf-8 'utf-8)
     (set-process-query-on-exit-flag p nil)))
 
+(defun lean-show-goal-at-pos ()
+  "Show goal at the current point. If the current point is a
+placeholder, call lean-server with --hole option, otherwise call
+  lean-server with --goal option"
+  (interactive)
+  (cond ((and (eq (char-after) ?_)               ;; 1. at _
+              (not (lean-in-comment-p))          ;; 2. not in comment
+              (or (bolp)                         ;; 3. either beginning of line
+                  (let ((cb (char-before)))      ;;    or whitespace
+                    (or (char-equal cb ?\s)
+                        (char-equal cb ?\t)
+                        (char-equal cb ?\n)
+                        (char-equal cb ?\r))))
+              (lean-exec-at-pos "lean-hole" "*Lean Goal*" "--hole"))
+         (t
+          (lean-exec-at-pos "lean-goal" "*Lean Goal*" "--goal"))))
+
 (defun lean-std-exe ()
   (interactive)
   (lean-execute))
@@ -186,11 +203,7 @@ will be flushed everytime it's executed."
   (local-set-key "\C-c\C-r"  'lean-server-restart-process)
   (local-set-key "\M-."      'lean-find-tag)
   (local-set-key (kbd "TAB") 'lean-tab-indent-or-complete)
-  (lean-define-key-binding "\C-c\C-p"
-                           '(lean-exec-at-pos "lean-hole" "*Lean Goal*" "--hole"))
-  (lean-define-key-binding "\C-c\C-g"
-                           '(lean-exec-at-pos "lean-goal" "*Lean Goal*" "--goal"))
-  )
+  (lean-define-key-binding "\C-c\C-g" '(lean-show-goal-at-pos)))
 
 (defun lean-define-key-binding (key cmd)
   (local-set-key key `(lambda () (interactive) ,cmd)))
diff --git a/src/emacs/lean-util.el b/src/emacs/lean-util.el
index 2285d93d0..07a582dfc 100644
--- a/src/emacs/lean-util.el
+++ b/src/emacs/lean-util.el
@@ -194,4 +194,9 @@
            'hott)
           (t 'standard))))
 
+(defun lean-in-comment-p ()
+  "t if a current point is inside of comment block
+   nil otherwise"
+  (nth 4 (syntax-ppss)))
+
 (provide 'lean-util)