A command to set coq printing width smartly.

Set the width to the current goals window.
Default binding: C-c C-a C-w.

3 files changed, 27 insertions, 1 deletions

diff --git a/CHANGES b/CHANGES
index d09b67cb..779f334a 100644
--- a/CHANGES
+++ b/CHANGES
@@ -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]
diff --git a/coq/coq.el b/coq/coq.el
index 22a145d5..61107c9d 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -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)