diff options
Diffstat (limited to 'generic')
| -rw-r--r-- | generic/pg-custom.el | 2 | ||||
| -rw-r--r-- | generic/pg-response.el | 15 | ||||
| -rw-r--r-- | generic/pg-vars.el | 2 | ||||
| -rw-r--r-- | generic/proof-config.el | 7 | ||||
| -rw-r--r-- | generic/proof-faces.el | 2 | ||||
| -rw-r--r-- | generic/proof-script.el | 11 | ||||
| -rw-r--r-- | generic/proof-shell.el | 45 | ||||
| -rw-r--r-- | generic/proof-site.el | 2 | ||||
| -rw-r--r-- | generic/proof-splash.el | 4 | ||||
| -rw-r--r-- | generic/proof-tree.el | 16 | ||||
| -rw-r--r-- | generic/proof-utils.el | 93 |
11 files changed, 129 insertions, 70 deletions
diff --git a/generic/pg-custom.el b/generic/pg-custom.el index efbc8a76..2edf320e 100644 --- a/generic/pg-custom.el +++ b/generic/pg-custom.el @@ -150,7 +150,7 @@ Completion is activated with \\[complete]. If this table is empty or needs adjusting, please make changes using `customize-variable' and post suggestions at -http://proofgeneral.inf.ed.ac.uk/trac" +https://github.com/ProofGeneral/PG/issues" :type '(repeat string) :group 'prover-config) diff --git a/generic/pg-response.el b/generic/pg-response.el index 46c7e1b5..893d1f6f 100644 --- a/generic/pg-response.el +++ b/generic/pg-response.el @@ -22,6 +22,7 @@ (defvar proof-assistant-menu nil)) (require 'pg-assoc) +(require 'span) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; @@ -157,23 +158,29 @@ Following POLICY, which can be one of 'smart, 'horizontal, (other-window 1) (switch-to-buffer b2) (proof-safe-split-window-vertically) ; enlarge vertically if necessary + (set-window-dedicated-p (selected-window) proof-three-window-enable) (other-window 1) - (switch-to-buffer b3)) + (switch-to-buffer b3) + (set-window-dedicated-p (selected-window) proof-three-window-enable)) ((eq pol 'vertical) (split-window-vertically) (other-window 1) (switch-to-buffer b2) (proof-safe-split-window-vertically) ; enlarge vertically if necessary + (set-window-dedicated-p (selected-window) proof-three-window-enable) (other-window 1) - (switch-to-buffer b3)) + (switch-to-buffer b3) + (set-window-dedicated-p (selected-window) proof-three-window-enable)) ((eq pol 'horizontal) (split-window-horizontally) ; horizontally again (other-window 1) (switch-to-buffer b2) (enlarge-window (/ (frame-width) 6) t) ; take 2/3 of width before splitting again (split-window-horizontally) ; horizontally again + (set-window-dedicated-p (selected-window) proof-three-window-enable) (other-window 1) - (switch-to-buffer b3)))))) + (switch-to-buffer b3) + (set-window-dedicated-p (selected-window) proof-three-window-enable)))))) @@ -270,7 +277,7 @@ dragging the separating bars. (proof-delete-all-associated-windows) (set-window-dedicated-p (selected-window) nil) (proof-display-three-b proof-three-window-mode-policy)) - ;; Two-of-three window mode. + ;; Two window mode. ;; Show the response buffer as first in preference order. (t ;; If we are coming from multiple frame mode, delete associated diff --git a/generic/pg-vars.el b/generic/pg-vars.el index 8dac2f11..3aafa97d 100644 --- a/generic/pg-vars.el +++ b/generic/pg-vars.el @@ -247,7 +247,7 @@ Internal variable dynamically bound.") :group 'proof-general-internals) (defcustom proof-general-home-page - "http://proofgeneral.inf.ed.ac.uk" + "https://proofgeneral.github.io" "*Web address for Proof General." :type 'string :group 'proof-general-internals) diff --git a/generic/proof-config.el b/generic/proof-config.el index b4898a35..8ce53168 100644 --- a/generic/proof-config.el +++ b/generic/proof-config.el @@ -1683,7 +1683,12 @@ tries to interrupt the proof process. It is therefore run earlier than `proof-shell-handle-error-or-interrupt-hook', which runs when the interrupt is acknowledged inside `proof-shell-exec-loop'. -This hook also runs when the proof assistent is killed." +This hook also runs when the proof assistent is killed. + +Hook functions should set the dynamic variable `prover-was-busy' +to t if there might have been a reason to interrupt. Otherwise +the generic interrupt handler might issue a prover-not-busy +error." :type '(repeat function) :group 'proof-shell) diff --git a/generic/proof-faces.el b/generic/proof-faces.el index 86cf7f0d..0eafc075 100644 --- a/generic/proof-faces.el +++ b/generic/proof-faces.el @@ -18,7 +18,7 @@ ;; But it's difficult to keep track of all that! ;; Please report any bad/failing colour ;; combinations (with suggested improvements) at -;; http://proofgeneral.inf.ed.ac.uk/trac +;; https://github.com/ProofGeneral/PG/issues ;; ;; Some of these faces aren't used by default in Proof General, ;; but you can use them in font lock patterns for specific diff --git a/generic/proof-script.el b/generic/proof-script.el index a9c55353..e67a7774 100644 --- a/generic/proof-script.el +++ b/generic/proof-script.el @@ -1989,11 +1989,12 @@ No effect if prover is busy." (proof-interrupt-process) (proof-shell-wait)) (save-excursion - (save-restriction ;; see Trac#403 - (widen) - (goto-char beg) - (proof-retract-until-point) - (proof-shell-wait))))) + (save-match-data ;; see PG#41 + (save-restriction ;; see Trac#403 + (widen) + (goto-char beg) + (proof-retract-until-point) + (proof-shell-wait)))))) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; diff --git a/generic/proof-shell.el b/generic/proof-shell.el index 64eee4c8..51038fa6 100644 --- a/generic/proof-shell.el +++ b/generic/proof-shell.el @@ -21,11 +21,20 @@ (require 'span) (require 'proof-utils)) +;; declare a few functions and variables from proof-tree - if we +;; require proof-tree the compiler complains about a recusive +;; dependency. +(declare-function proof-tree-urgent-action "proof-tree" (flags)) +(declare-function proof-tree-handle-delayed-output "proof-tree" + (old-proof-marker cmd flags span)) +(eval-when (compile) + ;; without the nil initialization the compiler still warns about this variable + (defvar proof-tree-external-display nil)) + (require 'scomint) (require 'pg-response) (require 'pg-goals) (require 'pg-user) ; proof-script, new-command-advance -(require 'proof-tree) ;; @@ -79,9 +88,11 @@ See the functions `proof-start-queue' and `proof-shell-exec-loop'.") (defsubst proof-shell-invoke-callback (listitem) "From `proof-action-list' LISTITEM, invoke the callback on the span." - (condition-case nil + (condition-case err (funcall (nth 2 listitem) (car listitem)) - (error nil))) + (error + (message "error escaping proof-shell-invoke-callback: %s" err) + nil))) (defvar proof-second-action-list-active nil "Signals that some items are waiting outside of `proof-action-list'. @@ -293,8 +304,10 @@ process command." (apply proof-guess-command-line (list name))))) (if proof-prog-name-ask - (setq proof-prog-name (read-shell-command "Run process: " - proof-prog-name))) + ;; if this option is set, an absolute file name is better to show if possible + (let ((prog-name (locate-file proof-prog-name exec-path exec-suffixes 1))) + (setq proof-prog-name (read-shell-command "Run process: " + prog-name)))) (let ((proc (downcase proof-assistant))) @@ -451,7 +464,9 @@ shell buffer, called by `proof-shell-bail-out' if process exits." (proc (get-buffer-process (current-buffer))) (bufname (buffer-name))) (message "%s, cleaning up and exiting..." bufname) - (run-hooks 'proof-shell-signal-interrupt-hook) + (let (prover-was-busy) + ;; hook functions might set prover-was-busy + (run-hooks 'proof-shell-signal-interrupt-hook)) (redisplay t) (when (and alive proc) @@ -813,14 +828,18 @@ In the first case, PG will terminate the queue of commands at the first available point. In the second case, you may need to press enter inside the prover command buffer (e.g., with Isabelle2009 press RET inside *isabelle*)." (interactive) - (unless (proof-shell-live-buffer) + (let ((prover-was-busy nil)) + (unless (proof-shell-live-buffer) (error "Proof process not started!")) - (unless proof-shell-busy - (error "Proof process not active!")) - (setq proof-shell-interrupt-pending t) - (with-current-buffer proof-shell-buffer - (interrupt-process)) - (run-hooks 'proof-shell-signal-interrupt-hook)) + ;; hook functions might set prover-was-busy + (run-hooks 'proof-shell-signal-interrupt-hook) + (if proof-shell-busy + (progn + (setq proof-shell-interrupt-pending t) + (with-current-buffer proof-shell-buffer + (interrupt-process))) + (unless prover-was-busy + (error "Proof process not active!"))))) diff --git a/generic/proof-site.el b/generic/proof-site.el index f2c9dafe..c2f9f480 100644 --- a/generic/proof-site.el +++ b/generic/proof-site.el @@ -72,7 +72,7 @@ (eval-and-compile ;; WARNING: do not edit next line (constant is edited in Makefile.devel) - (defconst proof-general-version "Proof General Version 4.4pre." + (defconst proof-general-version "Proof General Version 4.4.1~pre." "Version string identifying Proof General release.")) (defconst proof-general-short-version diff --git a/generic/proof-splash.el b/generic/proof-splash.el index 6bc20998..25db0946 100644 --- a/generic/proof-splash.el +++ b/generic/proof-splash.el @@ -70,8 +70,8 @@ Proof General." "PG is on Github at https://github.com/ProofGeneral/PG") :link '("or the " "homepage" (lambda (button) - (browse-url "http://proofgeneral.inf.ed.ac.uk/")) - "Browse http://proofgeneral.inf.ed.ac.uk/") + (browse-url "https://proofgeneral.github.io")) + "Browse https://proofgeneral.github.io") nil :link '("Find out about Emacs on the Help menu -- start with the " "Emacs Tutorial" (lambda (button) (help-with-tutorial))) diff --git a/generic/proof-tree.el b/generic/proof-tree.el index 03af645e..f0894656 100644 --- a/generic/proof-tree.el +++ b/generic/proof-tree.el @@ -556,7 +556,8 @@ Runs on process status changes and cleans up when prooftree dies." "Start the external prooftree process. Does also initialize the communication channel and some internal variables." - (let ((old-proof-tree (get-process proof-tree-process-name))) + (let ((process-connection-type nil) ; use pipes, see emacs bug #24531 + (old-proof-tree (get-process proof-tree-process-name))) ;; reset output marker (when proof-tree-output-marker (set-marker proof-tree-output-marker nil) @@ -841,13 +842,14 @@ The not yet delayed output is in the region (start proof-shell-delayed-output-start) (end proof-shell-delayed-output-end) inst-ex-vars) - (when (and (not (memq 'proof-tree-show-subgoal flags)) - (> state proof-tree-last-state)) - ;; Only deal with existentials if the proof assistant has them - ;; (i.e., proof-tree-existential-regexp is set) and if there are some - ;; goals with existentials. - (when (and proof-tree-existential-regexp + (unless (memq 'proof-tree-show-subgoal flags) + (when (and (> state proof-tree-last-state) + proof-tree-existential-regexp proof-tree-existentials-alist) + ;; Only deal with existentials if this is not and undo + ;; command, if the proof assistant actually has existentials + ;; (i.e., proof-tree-existential-regexp is set) and if there + ;; are some goals with existentials. (setq inst-ex-vars (with-current-buffer proof-shell-buffer (funcall proof-tree-extract-instantiated-existentials diff --git a/generic/proof-utils.el b/generic/proof-utils.el index f559eead..75ddbf69 100644 --- a/generic/proof-utils.el +++ b/generic/proof-utils.el @@ -220,43 +220,59 @@ Leave point at END." (unless (and (boundp sym) (symbol-value sym)) (warn "Proof General %s: %s is unset." tag (symbol-name sym)))) +(defvar proof-advertise-layout-freq 30 + "Frequency for PG messages to be displayed from time to time.") +(defvar proof-advertise-layout-count proof-advertise-layout-freq + "counter used to display PG messages from time to time.") + (defun proof-get-window-for-buffer (buffer) "Find a window for BUFFER, display it there, return the window. -NB: may change the selected window." +NB: may change the selected window. This function is a wrapper on +display-buffer. The idea is that if the user has opened and +closed some windows we want to preserve the layout by only +switching buffer in already pg-associate windows. So if the +buffer is not already displayed, we try to reuse an existing +associated window, even if in 3-win mode. If no such window +exists, we fall back to display-buffer while protecting script +buffer to be hidden or split. + +Experimentally we display a message from time to time advertising +C-c C-l." ;; IF there *isn't* a visible window showing buffer... (unless (get-buffer-window buffer 0) - ;; THEN find somewhere nice to display it - (if (and - ;; If we're in two-window mode and already displaying a - ;; script/response/goals, try to just switch the buffer - ;; instead of calling display-buffer which alters sizes. - ;; Gives user some stability on display. - (not proof-three-window-enable) - (> (count-windows) 1) - ;; was: (not (eq (next-window) (selected-window))) - (memq (window-buffer (next-window nil 'ignoreminibuf)) - ;; NB: 3.5: added rest of assoc'd buffers here - (cons proof-script-buffer (proof-associated-buffers)))) - (if (eq (selected-window) (minibuffer-window)) - ;; 17.8.01: avoid switching the minibuffer's contents - ;; -- terrrible confusion -- use next-window after - ;; script buffer instead. - ;; (another hack which is mostly right) - (set-window-buffer - (next-window - (car-safe (get-buffer-window-list proof-script-buffer)) - 'ignoreminibuf) buffer) - (if (eq (window-buffer (next-window nil 'ignoreminibuf)) - proof-script-buffer) - ;; switch this window - (set-window-buffer (selected-window) buffer) - ;; switch other window - (set-window-buffer (next-window nil 'ignoreminibuf) buffer))) - ;; o/w: call display buffer to configure windows nicely. - (display-buffer buffer))) + (if proof-three-window-enable + (if (< proof-advertise-layout-count 30) (incf proof-advertise-layout-count) + (message (substitute-command-keys "Hit \\[proof-layout-windows] to reset layout")) + (setq proof-advertise-layout-count 0))) + ;; THEN either we are in 2 wins mode and we must switch the assoc + ;; window to buffer OR we deleted a window by mistake and we + ;; behave as if in 2 win mode instead of calling display-buffer + ;; (stability for the user). If no assoc win exists then we are in + ;; trouble: let display-buffer decide but avoid hiding the script buffer. + (if (= (count-windows) 1) + ;; only one window: fallback to display-buffer + (display-buffer buffer) + ;; There is at least 2 windows, let us find some assoc ones. + (let* ((assoc-wins (proof-associated-windows)) + ;; may be nil if no assoc frame + (win-to-use (and assoc-wins (car assoc-wins)))) + ;; let us switch the buffer in this window even if protected (3-win mode) + (if win-to-use + (let ((prot (window-dedicated-p win-to-use))) + (set-window-dedicated-p win-to-use nil) + (set-window-buffer win-to-use buffer) + (set-window-dedicated-p win-to-use prot)) + ;; if no assoc win then let display-buffer decide but + ;; protect script buffer from disappearing. + (let ((win-proof-script (car-safe (get-buffer-window-list proof-script-buffer)))) + (set-window-dedicated-p win-proof-script t) ; avoid to hide script buffer at all cost + (let ((res (display-buffer buffer))) ; return this but revert the dedicated flag first + (set-window-dedicated-p win-proof-script nil) + res)))))) ;; Return the window, hopefully the one we first thought of. (get-buffer-window buffer 0)) + (defun proof-display-and-keep-buffer (buffer &optional pos force) "Display BUFFER and make window according to display mode. If optional POS is present, will set point to POS. @@ -330,7 +346,7 @@ If flag `proof-general-debug' is nil, do nothing." (with-current-buffer (get-buffer-create "*PG Debug*") (help-mode) (let ((formatted (apply 'format msg args)) - (log-warning-minimum-level :debug) + (warning-minimum-log-level :debug) (warning-minimum-level :debug) (buffer-read-only nil)) (display-warning 'proof-general @@ -431,14 +447,23 @@ or if the window is the only window of its frame." ;; buffers? Probably not an issue for us, but one ;; wonders at the shrink to fit strategy. ;; NB: way to calculate pixel fraction? - (+ extraline (count-lines (point-min) (point-max))))) + (+ extraline (count-lines (point-min) (point-max)))) + (safe-desired-height + ;; Under certain circumstances (involving a non-nil + ;; line-spacing), a desired-height of 1 (which happens + ;; quite often, eg for an empty response buffer) gives an + ;; error inside set-window-text-height. The reason for + ;; this is quite complicated, it involves rounding issues + ;; and emacs' habbit to sometimes resize a window by 2 + ;; pixels. + (max 2 desired-height))) ;; Let's shrink or expand. Uses new GNU Emacs function. (let ((window-size-fixed nil)) (set-window-text-height window ;; As explained earlier: use abs-max-height ;; but only if that makes it display all. - (if (> desired-height absolute-max-height) - max-height desired-height))) + (if (> safe-desired-height absolute-max-height) + max-height safe-desired-height))) (if (window-live-p window) (progn (if (>= (window-text-height window) desired-height) |