proof-assert-command-hook added + Auto adjust width in coq mode.

This hook was missing, it allows to send complete commands before
the (set of) command(s) sent by the user. It shall be used when
proof-shell-insert-hook cannot be used (because of multiple prompts
appearing).

5 files changed, 96 insertions, 23 deletions

diff --git a/CHANGES b/CHANGES
index 589a1b08..e5fc9357 100644
--- a/CHANGES
+++ b/CHANGES
@@ -122,13 +122,18 @@ 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
+*** Auto adjusting of printing width
 
-    (coq-adapt-printing-width) sets the coq printing width to the
-    width of goals window. Default binding: C-c C-a C-w.
+    On by default. To disable: Coq/Settings/Auto Adapt Printing Width. 
 
 *** Coq Querying facilities
 
+*** Removed the Set Undo 500 at start.
+    This is obsolete. To recover: (setq coq-user-init-cmd `("Set Undo 500."))
+
+
+
+
 **** Minibuffer interactive queries
 
     Menu Coq/Other Queries (C-c C-a C-q) allows to send queries (like
diff --git a/coq/coq-abbrev.el b/coq/coq-abbrev.el
index a088fba8..e664317f 100644
--- a/coq/coq-abbrev.el
+++ b/coq/coq-abbrev.el
@@ -172,7 +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 Width" coq-ask-adapt-printing-width-and-show 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 236af8f7..3ba0487a 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -111,8 +111,17 @@ Set to t if you want this feature."
   :type 'number
   :group 'coq)
 
+(defcustom coq-user-init-cmd nil
+  "user defined init commands for Coq.
+These are appended at the end of `coq-shell-init-cmd'."
+  :type '(repeat (cons (string :tag "command")))
+  :group 'coq)
+
+
+;TODO: remove Set Undo xx. It is obsolete since coq-8.5 at least.
+;;`(,(format "Set Undo %s . " coq-default-undo-limit) "Set Printing Width 75.")
 (defconst coq-shell-init-cmd
-  `(,(format "Set Undo %s . " coq-default-undo-limit) "Set Printing Width 75.") 
+  (append nil coq-user-init-cmd)
  "Command to initialize the Coq Proof Assistant.")
 
 (require 'coq-syntax)
@@ -770,7 +779,7 @@ Support dot.notation.of.modules."
              (coq-grab-punctuation-right pos)))))
 
 (defun coq-string-starts-with-symbol (s)
-  (eq 0 (string-match "\\s_" symbclean)))
+  (eq 0 (string-match "\\s_" s)))
 
 ;; remove trailing dot if any.
 (defun coq-id-at-point ()
@@ -837,7 +846,6 @@ Otherwise propose identifier at point if any."
            ((use-region-p)
             (buffer-substring-no-properties (region-beginning) (region-end)))
            (t (coq-id-or-notation-at-point)))))
-    (message "YOUHOU: %S" guess) 
     (read-string
      (if guess (concat s " (default " guess "): ") (concat s ": "))
      nil 'proof-minibuffer-history guess)))
@@ -1108,21 +1116,66 @@ flag Printing All set."
   (interactive)
   (coq-ask-do-show-all "Show goal number" "Show" t))
 
+;; Check
+(eval-when (compile)
+  (defvar coq-auto-adapt-printing-width nil)); defpacustom
+
+(defun coq-auto-adapt-printing-width-switch ()
+  "Function called when toggling `auto-adapt-printing-width'"
+  (if coq-auto-adapt-printing-width
+      (add-hook 'proof-assert-command-hook 'coq-adapt-printing-width)
+    (remove-hook 'proof-assert-command-hook 'coq-adapt-printing-width)))
+
+(add-hook 'proof-assert-command-hook 'coq-adapt-printing-width)
+
+(defpacustom auto-adapt-printing-width t
+  "If non-nil, adapt automatically printing width of goals window.
+Each timme the user sends abunch of commands to Coq, check if the
+width of the goals window changed, and adapt coq printing width.
+WARNING: If several windows are displaying the goals buffer, one
+is chosen randomly. WARNING 2: when backtracking the printing
+width is synchronized by coq (?!)."
+  :type 'boolean
+  :safe 'booleanp
+  :group 'coq
+  :eval (coq-auto-adapt-printing-width-switch))
+
+(defvar coq-shell-current-line-width nil
+  "Current line width of the Coq printing width.
+Its value will be updated whenever a command is sent if
+necessary.")
+
+(defun coq-goals-window-width ()
+  (let*
+      ((goals-wins (get-buffer-window-list proof-goals-buffer))
+       (dummy (if (not (eq 1 (length goals-wins)))
+                  (message "Zero or more than one goals window, guessing window width.")))
+       (goal-win (car goals-wins)))
+    (window-width goal-win)))
 
-(defun coq-adapt-printing-width ()
+(defun coq-adapt-printing-width (&optional show 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."
+A Show command is also issued if SHOW is non-nil, so that the
+goal is redisplayed."
+  (interactive)
+  (let ((wdth (or width (coq-goals-window-width))))
+    (when (not (equal wdth coq-shell-current-line-width))
+      (proof-shell-invisible-command (format "Set Printing Width %S." (- wdth 1)) t)
+      (setq coq-shell-current-line-width wdth)
+      ;; Show iff show non nil and some proof is under way
+      (when (and show (not (null (caddr (coq-last-prompt-info-safe)))))
+        (proof-shell-invisible-command (format "Show.") t nil 'no-error-display)))))
+
+(defun coq-adapt-printing-width-and-show(&optional show width)
+  (interactive)
+  (coq-adapt-printing-width t width))
+
+(defun coq-ask-adapt-printing-width-and-show ()
   (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)))
+  (let* ((deflt (coq-goals-window-width))
+         (rd (read-number (format "Width (%S): " deflt) deflt)))
+    (coq-adapt-printing-width t rd)))
+
 
 (defvar coq-highlight-id-last-regexp nil)
 
@@ -1407,6 +1460,8 @@ Warning:
                         (boundp 'show-paren-data-function))
                (setq show-paren-data-function 'show-paren--default))))
 
+
+
 (defun coq-toggle-use-project-file ()
   (interactive)
   (setq coq-use-project-file (not coq-use-project-file))
@@ -1964,7 +2019,6 @@ This is the Coq incarnation of `proof-tree-find-undo-position'."
 
 (add-hook 'proof-shell-insert-hook 'coq-preprocessing)
 
-
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;;
 ;; Subterm markup -- it was added to Coq by Healf, but got removed.
@@ -2308,7 +2362,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)
+(define-key coq-keymap [(control ?w)] 'coq-ask-adapt-printing-width-and-show)
 ;(proof-eval-when-ready-for-assistant
 ; (define-key ??? [(control c) (control a)] (proof-ass keymap)))
 
@@ -2326,7 +2380,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-goals-mode-map [(control ?c)(control ?a)(control ?w)] 'coq-ask-adapt-printing-width-and-show)
 (define-key coq-goals-mode-map [(control ?c)(control ?a)(control ?l)] 'coq-LocateConstant)
 (define-key coq-goals-mode-map [(control ?c)(control ?a)(control ?n)] 'coq-LocateNotation)
 
@@ -2341,7 +2395,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)
+(define-key coq-response-mode-map [(control ?c)(control ?a)(control ?w)] 'coq-ask-adapt-printing-width-and-show)
 (define-key coq-response-mode-map [(control ?c)(control ?a)(control ?l)] 'coq-LocateConstant)
 (define-key coq-response-mode-map [(control ?c)(control ?a)(control ?n)] 'coq-LocateNotation)
 
diff --git a/generic/proof-config.el b/generic/proof-config.el
index 43ca9a86..fc2dca86 100644
--- a/generic/proof-config.el
+++ b/generic/proof-config.el
@@ -1616,6 +1616,19 @@ it is added to the queue of commands."
   :type '(repeat function)
   :group 'proof-shell)
 
+(defcustom proof-assert-command-hook nil
+  "Hooks run before asserting a command (or a set of commands).
+Can be used to insert commands before any (set of) input sent
+by the user. It is run by `proof-assert-until-point'.
+
+WARNING: don't call `proof-assert-until-point' in this hook, you
+would loop forever.
+
+Example of use: Insert a command to adapt printing width. Note
+that `proof-shell-insert-hook' may be use instead (see lego mode)
+if no more prompt will be displayed (see
+`proof-shell-insert-hook' for details).")
+
 (defcustom proof-script-preprocess nil
   "Function to pre-process (SPAN STRING) taken from proof script."
   :type 'function
diff --git a/generic/proof-script.el b/generic/proof-script.el
index fbd8c2b1..338318e7 100644
--- a/generic/proof-script.el
+++ b/generic/proof-script.el
@@ -1912,6 +1912,7 @@ Assumes that point is at the end of a command."
 	(setq semis (cdr semis)))
     (if (null semis) ; maybe inside a string or something.
 	(error "I can't find any complete commands to process!"))
+    (run-hooks 'proof-assert-command-hook) ;; sneak commands (real ones with a prompt)
     (proof-assert-semis semis displayflags)))
 
 (defun proof-assert-electric-terminator ()