diff options
-rw-r--r-- | CHANGES | 5 | ||||
-rw-r--r-- | coq/coq-abbrev.el | 1 | ||||
-rw-r--r-- | coq/coq.el | 22 |
3 files changed, 27 insertions, 1 deletions
@@ -116,6 +116,11 @@ the CVS ChangeLog and PG Trac, http://proofgeneral.inf.ed.ac.uk/trac. Experimental: colorize hypothesis names and some parts of error and warning messages. For readability. +*** Set Printing Width adapted to goals window size + + (coq-adapt-printing-width) sets the coq printing width to the + width of goals window. Default binding: C-c C-a C-w. + *** Coq Querying facilities **** Minibuffer interactive queries diff --git a/coq/coq-abbrev.el b/coq/coq-abbrev.el index 431f463f..a088fba8 100644 --- a/coq/coq-abbrev.el +++ b/coq/coq-abbrev.el @@ -172,6 +172,7 @@ ["UnSet Printing All" coq-unset-printing-all t] ["Set Implicit Argument" coq-set-implicit-arguments t] ["Unset Implicit Argument" coq-unset-implicit-arguments t] + ["Adapt Printing Width" coq-adapt-printing-width t] ["Set Printing Synth" coq-set-printing-synth t] ["Unset Printing Synth" coq-unset-printing-synth t] ["Set Printing Coercions" coq-set-printing-coercions t] @@ -1091,6 +1091,22 @@ flag Printing All set." (coq-ask-do-show-all "Show goal number" "Show" t)) +(defun coq-adapt-printing-width () + "Sends a Set Printing Width command to coq to fit the response window's width. +A Show command is also issued, so that the goal is redisplayed." + (interactive) + (let* ((goals-wins (get-buffer-window-list proof-goals-buffer)) + (dummy (if (not (eq 1 (length goals-wins))) + (error "Zero or more than one goals window"))) + (goal-win (car goals-wins)) + (wdth + (save-selected-window + (select-window goal-win) + (window-width)))) + (proof-shell-invisible-command (format "Set Printing Width %S." (- wdth 1)) t) + (proof-shell-invisible-command (format "Show.") t))) + + (proof-definvisible coq-PrintHint "Print Hint. ") ;; Items on show menu @@ -1112,6 +1128,8 @@ flag Printing All set." ;(proof-definvisible coq-set-printing-printing-depth "Set Printing Printing Depth . ") ;(proof-definvisible coq-unset-printing-printing-depth "Unset Printing Printing Depth . ") + + (defun coq-Compile () "Compiles current buffer." (interactive) @@ -2150,7 +2168,7 @@ Completion is on a quasi-exhaustive list of Coq tacticals." (define-key coq-keymap [?h] 'coq-PrintHint) (define-key coq-keymap [(control ?l)] 'coq-LocateConstant) (define-key coq-keymap [(control ?n)] 'coq-LocateNotation) - +(define-key coq-keymap [(control ?w)] 'coq-adapt-printing-width) ;(proof-eval-when-ready-for-assistant ; (define-key ??? [(control c) (control a)] (proof-ass keymap))) @@ -2168,6 +2186,7 @@ Completion is on a quasi-exhaustive list of Coq tacticals." (define-key coq-goals-mode-map [(control ?c)(control ?a)?g] 'proof-store-goals-win) (define-key coq-goals-mode-map [(control ?c)(control ?a)?h] 'coq-PrintHint) (define-key coq-goals-mode-map [(control ?c)(control ?a)(control ?q)] 'coq-query) +(define-key coq-goals-mode-map [(control ?c)(control ?a)(control ?w)] 'coq-adapt-printing-width) (define-key coq-response-mode-map [(control ?c)(control ?a)(control ?c)] 'coq-Check) @@ -2180,6 +2199,7 @@ Completion is on a quasi-exhaustive list of Coq tacticals." (define-key coq-response-mode-map [(control ?c)(control ?a)(control ?g)] 'proof-store-goals-win) (define-key coq-response-mode-map [(control ?c)(control ?a)?h] 'coq-PrintHint) (define-key coq-response-mode-map [(control ?c)(control ?a)(control ?q)] 'coq-query) +(define-key coq-response-mode-map [(control ?c)(control ?a)(control ?w)] 'coq-adapt-printing-width) (when coq-remap-mouse-1 (define-key proof-mode-map [(control down-mouse-1)] 'coq-id-under-mouse-query) |