From 72f0fc29fd115ea5bb919afa2acffdf796c9fa5d Mon Sep 17 00:00:00 2001 From: Soonho Kong Date: Tue, 28 Jul 2015 11:13:31 -0700 Subject: [PATCH] fix(emacs/lean-mode.el): check header and footer in lean-exec-at-pos-extract-body close #747 --- src/emacs/lean-mode.el | 22 ++++++++++++++-------- 1 file changed, 14 insertions(+), 8 deletions(-) diff --git a/src/emacs/lean-mode.el b/src/emacs/lean-mode.el index 8c1b14d5d1..063f5700bb 100644 --- a/src/emacs/lean-mode.el +++ b/src/emacs/lean-mode.el @@ -59,14 +59,20 @@ (defun lean-exec-at-pos-extract-body (str) "Extract the body of LEAN_INFORMATION" - (let* - ((begin-regex (rx line-start "LEAN_INFORMATION" (* not-newline) line-end)) - (end-regex (rx line-start (group "END_LEAN_INFORMATION") line-end)) - (pre-body-post - (lean-server-split-buffer str begin-regex end-regex)) - (body (cadr pre-body-post)) - (lines (s-lines body))) - (s-join "\n" (-butlast (-drop 1 lines))))) + (let ((header "LEAN_INFORMATION") + (footer "END_LEAN_INFORMATION")) + (cond + ((and (s-contains? header str) + (s-contains? footer str)) + (let* + ((begin-regex (eval `(rx line-start ,header (* not-newline) line-end))) + (end-regex (eval `(rx line-start (group ,footer) line-end))) + (pre-body-post + (lean-server-split-buffer str begin-regex end-regex)) + (body (cadr pre-body-post)) + (lines (s-lines body))) + (s-join "\n" (-butlast (-drop 1 lines))))) + (t "")))) (defun lean-exec-at-pos-sentinel (process event) "Sentinel function used for lean-exec-at-pos. It does the two