From 096f11ea25419bfa0b44a56d012a5237fb6f2f38 Mon Sep 17 00:00:00 2001 From: Clément Pit--Claudel Date: Thu, 14 Apr 2016 14:15:26 -0400 Subject: Respect user settings in coq-insert-intros Fixes #67. --- coq/coq.el | 28 ++++++++++++++++++---------- 1 file changed, 18 insertions(+), 10 deletions(-) diff --git a/coq/coq.el b/coq/coq.el index 6c745604..49d72c16 100644 --- a/coq/coq.el +++ b/coq/coq.el @@ -2052,20 +2052,28 @@ mouse activation." (progn (end-of-line) (point))))))) (insert (concat "End" section))))) +(defun coq--format-intros (output) + "Create an “intros” form from the OUTPUT of “Show Intros”." + (let* ((shints (replace-regexp-in-string "[\r\n ]*\\'" "" output))) + (if (or (string-empty-p shints) + (string-match coq-error-regexp shints)) + (error "Don't know what to intro") + (format "intros %s" shints)))) + (defun coq-insert-intros () "Insert an intros command with names given by Show Intros. Based on idea mentioned in Coq reference manual." (interactive) - (let* ((shints (proof-shell-invisible-cmd-get-result "Show Intros.")) - ;; insert a dot before the trailing \n and put intros at begining - (intros (concat "intros " (substring shints 0 (- (length shints) 1)) ".\n"))) - (if (or (< (length shints) 2);; empty response is just NL - (string-match coq-error-regexp shints)) - (error "Don't know what to intro") - (let ((pt (point))) - (insert intros) - (indent-region pt (point)))))) - + (let* ((output (proof-shell-invisible-cmd-get-result "Show Intros."))) + (indent-region (point) + (progn (insert (coq--format-intros output)) + (save-excursion + (insert (if coq-one-command-per-line "\n" " ")) + (point)))) + ;; `proof-electric-terminator' moves the point in all sorts of strange + ;; ways, so we run it last + (let ((last-command-event ?.)) ;; Insert a dot + (proof-electric-terminator)))) (defvar coq-keywords-accepting-as-regex (regexp-opt '("induction" "destruct" "inversion" "injection"))) -- cgit v1.2.3