diff options
| -rw-r--r-- | CHANGES | 40 | ||||
| -rw-r--r-- | coq/coq-abbrev.el | 46 | ||||
| -rw-r--r-- | coq/coq.el | 74 | ||||
| -rw-r--r-- | generic/pg-response.el | 2 | ||||
| -rw-r--r-- | generic/proof-utils.el | 14 |
5 files changed, 124 insertions, 52 deletions
@@ -28,13 +28,27 @@ the CVS ChangeLog and PG Trac, http://proofgeneral.inf.ed.ac.uk/trac. ** Coq changes -*** Multiple file handling for Coq Feature. +*** Smarter three windows mode: + When the frame is not large enough, the three windows are + displayed vertically, otherwise goals and response buffers are + displayed on the right. C-c C-l to refresh after resizing the + frame. + + If you want to always have goals and response buffers displayed on + the right: + (setq proof-three-window-mode-policy 'horizontal). + Always three buffers diaplayed vertically: + (setq proof-three-window-mode-policy 'vertical). + + Or via customization menus. +*** Multiple file handling for Coq Feature. No more experimental. Set coq-load-path to the list of directories for libraries (you can attach it to the file using menu "coq prog - args"). + args"). Many thanks to Hendrik Tews for that great peace of code! *** Support proof-tree visualization + Many thanks to Hendrik Tews for that too! *** New commands for Print/Check/About/Show with "Printing All" flag Avoids typing "Printing All" in the buffer. See the menu Coq > @@ -46,9 +60,8 @@ the CVS ChangeLog and PG Trac, http://proofgeneral.inf.ed.ac.uk/trac. Check. Unset Printing All. ) -*** Coq menu visible in Response and goals buffers. - Shortcuts available too (Check, Print etc.) in response and goals - buffers. +*** Coq menus and shortcut in response and goals buffers. + Check, Print etc available in these buffers. *** Tooltips hidden by default Flickering when hovering commands is off by default! @@ -58,12 +71,18 @@ the CVS ChangeLog and PG Trac, http://proofgeneral.inf.ed.ac.uk/trac. *** New setting for hiding additional goals from the *goals* buffer Coq > Settings > Hide additional subgoals +*** Double hit terminator + Experimental: Same as electric terminator except you have to type + "." twice quickly. Electric terminator will stop getting in the + way all the time with module.notations. + Coq > Double Hit Electric Terminator. + *** Indentation improvements using SMIE. Supporting bullets and { }. Still experimental. Please submit bugs. -**** Limitations of indentation: + IMPORTANT: Limitations of indentation: -***** hard-wired precedence between bullets: - < + < * + - hard-wired precedence between bullets: - < + < * example: Proof. - split. @@ -75,9 +94,10 @@ the CVS ChangeLog and PG Trac, http://proofgeneral.inf.ed.ac.uk/trac. - auto. Qed. -***** Always use "Proof." when proving an "Instance". (wrong - indentation and slow downs otherwise) As a general rule, try to - always introduce a proof with "Proof." (or "Next Obligation"). + - Always use "Proof." when proving an "Instance" (wrong + indentation and slow downs otherwise). As a general rule, try to + always introduce a proof with "Proof." (or "Next Obligation" + with Program). *** Minor parsing fixes *** Windows resizing fixed 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 @@ -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) diff --git a/generic/pg-response.el b/generic/pg-response.el index 561436b0..40ed9ae8 100644 --- a/generic/pg-response.el +++ b/generic/pg-response.el @@ -121,7 +121,7 @@ Following POLICY, which can be one of 'smart, 'horizontal, 'vertical." (split-window-horizontally) (other-window 1) (switch-to-buffer b2)) - ((eq policy 'vertically) + ((eq policy 'vertical) (split-window-vertically) (other-window 1) (switch-to-buffer b2)) diff --git a/generic/proof-utils.el b/generic/proof-utils.el index 54dae790..f559eead 100644 --- a/generic/proof-utils.el +++ b/generic/proof-utils.el @@ -253,19 +253,7 @@ NB: may change the selected window." ;; switch other window (set-window-buffer (next-window nil 'ignoreminibuf) buffer))) ;; o/w: call display buffer to configure windows nicely. - ;; PC: Experimental this was simply (display-buffer buffer) but I am - ;; experimenting the following policy: when in three windows - ;; mode, always make new windo on the right pane, that is: - ;; always split one of the associated buffers windows - ;; this is not perfect, let's see if people like it - (let ((associated-windows (proof-associated-windows))) - (if (not (and proof-three-window-enable associated-windows)) - (display-buffer buffer) - (select-window (car associated-windows)) ; take on assoc. win - (proof-safe-split-window-vertically) - (set-window-dedicated-p (selected-window) nil) - (switch-to-buffer buffer) - (set-window-dedicated-p (selected-window) t))))) + (display-buffer buffer))) ;; Return the window, hopefully the one we first thought of. (get-buffer-window buffer 0)) |