From 22c3951cfdf4938fa6df7368daed7bead05e4592 Mon Sep 17 00:00:00 2001 From: Pierre Courtieu Date: Thu, 26 Nov 2015 17:32:01 +0100 Subject: A shortcut for coq-insert-as-in-next-command. Works well for a single induction/destruct. Works sometimes for inversion. Does not work in presence of eqn flag yet (easy to fix). Does not work on ;-combined tactics (hard to fix). Does not work on a lot of inversion invocation (but some are ok). We basically need another "as" tactical with a retro-predictable input. That is: when seeing the resulting goal we can deduce what would have been the right "as" close. This is currently the case only for destruct/induction !foo (notice the exclamation mark). --- coq/coq.el | 21 +++++++++++++-------- 1 file changed, 13 insertions(+), 8 deletions(-) (limited to 'coq') diff --git a/coq/coq.el b/coq/coq.el index d9a04bc5..9c55a195 100644 --- a/coq/coq.el +++ b/coq/coq.el @@ -2313,14 +2313,15 @@ Warning: this makes the error messages (and location) wrong.") ;; Trying to propose insertion of "as" for a whole region. But iterating ;; proof-assert-next-command-interactive is probably wrong if some error occur ;; during scripting. -(defun coq-insert-as-in-region (&optional beg end) - (interactive "r") - (let ((beg (or beg (point-min))) - (end (or end (point-max)))) - (goto-char beg) - (while (< (point) end) - (coq-script-parse-cmdend-forward) - (proof-assert-next-command-interactive)))) +;; (defun coq-insert-as-in-region (&optional beg end) +;; (interactive "r") +;; (let ((beg (or beg (point-min))) +;; (end (or end (point-max)))) +;; (goto-char beg) +;; (while (< (point) end) +;; (coq-script-parse-cmdend-forward) +;; (coq-insert-as-in-next-command) +;; (proof-assert-next-command-interactive)))) @@ -2404,6 +2405,9 @@ Completion is on a quasi-exhaustive list of Coq tacticals." (define-key coq-keymap [(control return)] 'coq-insert-command) (define-key coq-keymap [(control ?q)] 'coq-query) (define-key coq-keymap [(control ?r)] 'coq-insert-requires) +; [ for "as [xxx]" is easy to remember, ccontrol-[ would be better but hard to type on french keyboards +; anyway company-coq should provide an "as!". +(define-key coq-keymap [(?\[)] 'coq-insert-as-in-next-command) ;; not for goal/response buffer? ; Query commands (define-key coq-keymap [(control ?s)] 'coq-Show) @@ -2419,6 +2423,7 @@ Completion is on a quasi-exhaustive list of Coq tacticals." (define-key coq-keymap [(control ?l)] 'coq-LocateConstant) (define-key coq-keymap [(control ?n)] 'coq-LocateNotation) (define-key coq-keymap [(control ?w)] 'coq-ask-adapt-printing-width-and-show) + ;(proof-eval-when-ready-for-assistant ; (define-key ??? [(control c) (control a)] (proof-ass keymap))) -- cgit v1.2.3