diff options
| -rw-r--r-- | CHANGES | 11 | ||||
| -rw-r--r-- | coq/coq-abbrev.el | 2 | ||||
| -rw-r--r-- | coq/coq.el | 92 | ||||
| -rw-r--r-- | generic/proof-config.el | 13 | ||||
| -rw-r--r-- | generic/proof-script.el | 1 |
5 files changed, 96 insertions, 23 deletions
@@ -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] @@ -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 () |