Fixed double hit terminator. Now it is disabled by default, and

enabling it disables electric-terminator and vice-versa. In case both
are non nil at the same time, then electric teminator has priority. If
people like it we may propose this to other modes than coq.

+ fixed window layout policy.

2 files changed, 92 insertions, 28 deletions

diff --git a/coq/coq-abbrev.el b/coq/coq-abbrev.el
index aad46d45..6bd687ef 100644
--- a/coq/coq-abbrev.el
+++ b/coq/coq-abbrev.el
@@ -80,27 +80,35 @@
 ;; Common part (scrit, response and goals buffers)
 (defconst coq-menu-common-entries
   `(
-    ["Toggle 3 windows mode" proof-three-window-toggle 
+    ["Toggle 3 Windows Mode" proof-three-window-toggle 
      :style toggle
      :selected proof-three-window-enable
      :help "Toggles the use of separate windows or frames for Coq responses and goals."
      ]
-    ["Refresh windows layout" proof-layout-windows t]
+    ["Refresh Windows Layout" proof-layout-windows t]
     ["Toggle tooltips" proof-output-tooltips-toggle
      :style toggle
      :selected proof-output-tooltips
-     :help "Toggles tooltips (popup when hovering commands).\nSet `proof-output-tooltips' to nil to disable it by default."]
+     :help "Toggles Tooltips (popup when hovering commands).\nSet `proof-output-tooltips' to nil to disable it by default."]
+    ["Electric Terminator" proof-electric-terminator-toggle
+     :style toggle
+     :selected proof-electric-terminator-enable
+     :help "Automatically send commands when terminator typed"]
+    ["Double Hit Electric Terminator" coq-double-hit-toggle
+     :style toggle
+     :selected coq-double-hit-enable
+     :help "Automatically send commands when terminator typed twiced quickly."]
     ""
     ["Print..." coq-Print :help "With prefix arg (C-u): Set Printing All first"]
     ["Check..." coq-Check :help "With prefix arg (C-u): Set Printing All first"]
     ["About..." coq-About :help "With prefix arg (C-u): Set Printing All first"]
-    [ "Store response" proof-store-response-win :help "Stores the content of response buffer in a dedicated buffer"]
-    [ "Store goal" proof-store-goals-win  :help "Stores the content of goals buffer in a dedicated buffer"]
+    [ "Store Response" proof-store-response-win :help "Stores the content of response buffer in a dedicated buffer"]
+    [ "Store Goal" proof-store-goals-win  :help "Stores the content of goals buffer in a dedicated buffer"]
     ("OTHER QUERIES"
      ["Print Hint" coq-PrintHint t]
-     ["Show ith goal..." coq-Show t]
-     ["Show ith goal... (show implicits)" coq-Show-with-implicits t]
-     ["Show ith goal... (show all)" coq-Show-with-all t]
+     ["Show ith Goal..." coq-Show t]
+     ["Show ith Goal... (show implicits)" coq-Show-with-implicits t]
+     ["Show ith Goal... (show all)" coq-Show-with-all t]
      ["Show Tree" coq-show-tree t]
      ["Show Proof" coq-show-proof t]
      ["Show Conjectures" coq-show-conjectures t];; maybe not so useful with editing in PG?
@@ -135,10 +143,10 @@
     ("INSERT"
      ["Intros (smart)" coq-insert-intros :help "Insert \"intros h1 .. hn.\" where hi are the default names given by Coq."]
      ""
-     ["tactic (interactive)" coq-insert-tactic t]
-     ["tactical (interactive)" coq-insert-tactical t]
-     ["command (interactive)" coq-insert-command t]
-     ["term (interactive)" coq-insert-term t]
+     ["Tactic (interactive)" coq-insert-tactic t]
+     ["Tactical (interactive)" coq-insert-tactical t]
+     ["Command (interactive)" coq-insert-command t]
+     ["Term (interactive)" coq-insert-term t]
      ""
      ,coq-tactics-menu
      ,coq-tacticals-menu
@@ -149,17 +157,17 @@
      ["Require (smart)" coq-insert-requires t])
     ""
     ("ABBREVS"
-     ["Expand at point" expand-abbrev t]
-     ["Unexpand last" unexpand-abbrev t]
-     ["List abbrevs" list-abbrevs t]
-     ["Edit abbrevs" edit-abbrevs t]
-     ["Abbrev mode" abbrev-mode
+     ["Expand At Point" expand-abbrev t]
+     ["Unexpand Last" unexpand-abbrev t]
+     ["List Abbrevs" list-abbrevs t]
+     ["Edit Abbrevs" edit-abbrevs t]
+     ["Abbrev Mode" abbrev-mode
       :style toggle
       :selected (and (boundp 'abbrev-mode) abbrev-mode)])
     ""
     ("COQ PROG (ARGS)"
-     ["Set coq prog *persistently*" coq-ask-insert-coq-prog-name t]
-     ["help on setting persistently" coq-local-vars-list-show-doc t]
+     ["Set Coq Prog *persistently*" coq-ask-insert-coq-prog-name t]
+     ["help" coq-local-vars-list-show-doc t]
      ["Compile" coq-Compile t]))))
 
 (defpgdefault help-menu-entries
diff --git a/coq/coq.el b/coq/coq.el
index ce43bef2..49db8d06 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -871,14 +871,23 @@ must be in locked region."
       (span-property (span-at (point) 'response) 'response))))
 
 (defun coq-Show (withprintingall)
-  "Ask for a number i and show the ith goal, or show ancient goal.
-If point is on a locked span, show the corresponding coq
-output (i.e. for tactics: the goal after the tactic). Otherwise
-ask for a number i and show the ith current goal. With non-nil
+  "Ask for a number i and show the ith goal.
+Ask for a number i and show the ith current goal. With non-nil
 prefix argument and not on the locked span, show the goal with
 flag Printing All set."
+; Disabled:
+;  "Ask for a number i and show the ith goal, or show ancient goal.
+;If point is on a locked span, show the corresponding coq
+;output (i.e. for tactics: the goal after the tactic). Otherwise
+;ask for a number i and show the ith current goal. With non-nil
+;prefix argument and not on the locked span, show the goal with
+;flag Printing All set."
+;
   (interactive "P")
-  (if (proof-in-locked-region-p)
+  ;; Disabling this as this relies on 'response attribute that is empty when
+  ;; the command was processed silently. We should first have a coq command
+  ;; asking to print the goal at a given state.
+  (if nil ;(proof-in-locked-region-p)
       (let ((s (coq-get-response-string-at)))
         (set-buffer proof-response-buffer)
         (let ((inhibit-read-only 'titi))
@@ -2634,6 +2643,9 @@ number of hypothesis displayed, without hiding the goal"
 ;; three window mode needs to be called when starting the script
 (add-hook 'proof-activate-scripting-hook '(lambda () (when proof-three-window-enable (proof-layout-windows))))
 
+;; three window mode needs to be called when starting the script
+(add-hook 'proof-activate-scripting-hook '(lambda () (when proof-three-window-enable (proof-layout-windows))))
+
 ;; *Experimental* auto shrink response buffer in three windows mode. Things get
 ;; a bit messed up if the response buffer is not at the right place (below
 ;; goals buffer) TODO: Have this linked to proof-resize-window-tofit in
@@ -2677,6 +2689,34 @@ Only when three-buffer-mode is enabled."
 
 
 ;; Trying to have double hit on colon behave like electric terminator.
+; TODO Have the same for other commands, but with insertion at all.
+
+(defcustom coq-double-hit-enable nil
+  "* Experimental: Whether or not double hit should be enabled in coq mode.
+A double hit is performed by pressing twice a key quickly. If
+this variable is not nil, then 1) it means that electric
+terminator is off and 2) a double hit on the terminator act as
+the usual electric terminator. See `proof-electric-terminator'.
+"
+  :type 'boolean
+  :set 'proof-set-value
+  :group 'proof-user-options)
+
+ (defun coq-double-hit-enable ()
+   "Disables electric terminator since double hit is a replacement.
+This function is called by `proof-set-value' on `coq-double-hit-enable'."
+   (when (and coq-double-hit-enable proof-electric-terminator-enable)
+     (proof-electric-terminator-toggle 0)))
+
+(proof-deftoggle coq-double-hit-enable coq-double-hit-toggle)
+
+(defadvice proof-electric-terminator-enable (after coq-unset-double-hit-advice)
+  "Disable double hit terminator since electric terminator is a replacement.
+This is an advice to pg `proof-electric-terminator-enable' function."
+  (when (and coq-double-hit-enable proof-electric-terminator-enable)
+    (coq-double-hit-toggle 0)))
+
+(ad-activate 'proof-electric-terminator-enable)
 
 (defvar coq-double-hit-delay 0.25
   "The maximum delay between the two hit of a double hit in coq/proofgeneral.")
@@ -2689,12 +2729,16 @@ Only when three-buffer-mode is enabled."
 
 
 (defun coq-unset-double-hit-hot ()
-  (unless (null coq-double-hit-timer)
-    (cancel-timer coq-double-hit-timer))
+  "Disable timer `coq-double-hit-timer' and set it to nil. Shut
+off the current double hit if any. This function is supposed to
+be called at double hit timeout."
+  (when coq-double-hit-timer (cancel-timer coq-double-hit-timer))
   (setq coq-double-hit-hot nil)
   (setq coq-double-hit-timer nil))
 
 (defun coq-colon-self-insert ()
+  "Detect a double hit and act as electric terminator if detected.
+Starts a timer for a double hit otherwise."
   (interactive)
   (if coq-double-hit-hot
       (progn (coq-unset-double-hit-hot)
@@ -2706,8 +2750,20 @@ Only when three-buffer-mode is enabled."
           (run-with-timer coq-double-hit-delay
                           nil 'coq-unset-double-hit-hot))))
 
-(define-key coq-mode-map (kbd ".") 'coq-colon-self-insert)
-(define-key coq-mode-map (kbd ";") 'coq-colon-self-insert) ; for french keyboards
+(defun coq-terminator-insert (&optional count)
+  "A wrapper on `proof-electric-terminator' to accept double hits instead if enabled.
+If by accident `proof-electric-terminator-enable' and `coq-double-hit-enable'
+are non-nil at the same time, this gives priority to the former."
+  (interactive)
+  (if proof-electric-terminator-enable (proof-electric-terminator count)
+    (if (and coq-double-hit-enable (null count))
+        (coq-colon-self-insert)
+      (self-insert-command (or count 1)))))
+
+;; Setting the new mapping for terminator
+(define-key coq-mode-map (kbd ".") 'coq-terminator-insert)
+;(define-key coq-mode-map (kbd ";") 'coq-terminator-insert) ; for french keyboards
+
 
 (provide 'coq)