diff options
author | Pierre Courtieu <courtieu@lri.fr> | 2012-10-02 16:23:34 +0000 |
---|---|---|
committer | Pierre Courtieu <courtieu@lri.fr> | 2012-10-02 16:23:34 +0000 |
commit | 75d8fe55b4108940e6b7be23a1f968e37c3b0873 (patch) | |
tree | fb3450fb78ee5298b5fcde6deb94b2191a6f7e03 | |
parent | 90d04c6966acde762a9f6f20d8af7286c99792e5 (diff) |
Made 'as' automatic insertion a togglable feature (not finished) (2).
-rw-r--r-- | coq/coq.el | 24 |
1 files changed, 13 insertions, 11 deletions
@@ -2369,9 +2369,13 @@ Based on idea mentioned in Coq reference manual." (indent-according-to-mode)))) +(defvar coq-command-accepting-as (regexp-opt '("destruct" "inversion" "injection"))) + (defun coq-insert-infoH-hook () - (with-no-warnings ;; NB: dynamic scoping of `string' - (setq string (concat "infoH " string)))) + (if (and (eq action 'proof-done-advancing) + (string-match coq-command-accepting-as string)) + (with-no-warnings ;; NB: dynamic scoping of `string' + (setq string (concat "infoH " string))))) (defcustom coq-auto-insert-as-enable nil "Don't set it manually, use `coq-auto-insert-as-toggle' instead." @@ -2382,8 +2386,11 @@ Based on idea mentioned in Coq reference manual." (defun coq-auto-insert-as-toggle () "Toggles coq automatic insertion of \"as\" closes." (if coq-auto-insert-as-enable - (remove-hook 'proof-shell-insert-hook 'coq-insert-infoH-hook) - (add-hook 'proof-shell-insert-hook 'coq-insert-infoH-hook)) + (progn + (remove-hook 'proof-shell-insert-hook 'coq-insert-infoH-hook) + (remove-hook 'proof-state-change-hook 'coq-insert-as)) + (add-hook 'proof-shell-insert-hook 'coq-insert-infoH-hook) + (add-hook 'proof-state-change-hook 'coq-insert-as)) (setq coq-auto-insert-as-enable (not coq-auto-insert-as-enable))) ;; Point supposed to be at the end of locked region, that is @@ -2413,15 +2420,12 @@ Based on idea mentioned in Coq reference manual. ; (proof-shell-wait) (when (and proof-goals-buffer proof-shell-last-output) (let* - ( - (str (string-match "<infoH>\\([^<]*\\)</infoH>" + ((str (string-match "<infoH>\\([^<]*\\)</infoH>" ;proof-shell-last-response-output would be better but ;since this message is output *before* resulting ;goals, it is not detected as a response message. proof-shell-last-output)) - (substr (or (and str (match-string 1 proof-shell-last-output)) "") - ) - ) ; idem + (substr (or (and str (match-string 1 proof-shell-last-output)) ""))) ; idem (unless (or (= (length substr) 0) (coq-tactic-already-has-an-as-close)) (save-excursion @@ -2430,8 +2434,6 @@ Based on idea mentioned in Coq reference manual. (insert (concat " as [" substr "]"))))) ))) -(add-hook 'proof-state-change-hook 'coq-insert-as) -;(add-hook 'proof-shell-handle-delayed-output-hook 'coq-insert-as) |