diff options
Diffstat (limited to 'generic')
| -rw-r--r-- | generic/pg-custom.el | 2 | ||||
| -rw-r--r-- | generic/pg-response.el | 49 | ||||
| -rw-r--r-- | generic/pg-user.el | 6 | ||||
| -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 | 19 | ||||
| -rw-r--r-- | generic/proof-shell.el | 50 | ||||
| -rw-r--r-- | generic/proof-site.el | 6 | ||||
| -rw-r--r-- | generic/proof-splash.el | 64 | ||||
| -rw-r--r-- | generic/proof-tree.el | 16 | ||||
| -rw-r--r-- | generic/proof-utils.el | 93 |
12 files changed, 184 insertions, 132 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 b0cf217d..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 @@ -393,23 +400,23 @@ Returns non-nil if response buffer was cleared." (t (let (start end) (with-current-buffer proof-response-buffer - (setq buffer-read-only nil) - ;; da: I've moved newline before the string itself, to match - ;; the other cases when messages are inserted and to cope - ;; with warnings after delayed output (non newline terminated). - (goto-char (point-max)) - ;; insert a newline before the new message unless the - ;; buffer is empty or proof-script-insert-newlines is nil - (unless (or (not proof-script-insert-newlines) - (eq (point-min) (point-max))) - (newline)) - (setq start (point)) - (insert str) - (unless (bolp) (newline)) - (when face - (overlay-put - (make-overlay start (point-max)) - 'face face)) + (setq buffer-read-only nil) + ;; da: I've moved newline before the string itself, to match + ;; the other cases when messages are inserted and to cope + ;; with warnings after delayed output (non newline terminated). + (goto-char (point-max)) + ;; insert a newline before the new message unless the + ;; buffer is empty or proof-script-insert-newlines is nil + (unless (or (not proof-script-insert-newlines) + (eq (point-min) (point-max))) + (newline)) + (setq start (point)) + (insert str) + (unless (bolp) (newline)) + (when face + (overlay-put + (span-make start (point-max)) + 'face face)) (setq buffer-read-only t) (set-buffer-modified-p nil)))))) diff --git a/generic/pg-user.el b/generic/pg-user.el index f0358239..513b477b 100644 --- a/generic/pg-user.el +++ b/generic/pg-user.el @@ -1273,7 +1273,11 @@ assuming the undo-in-region behavior will apply if ARG is non-nil." buffer-undo-list))) ; can be nil (if (or (null undo-list) (equal undo-list (list nil))) nil ; there is clearly no undo elt - (while (eq (car undo-list) nil) + (while (and undo-list ; to ensure it will terminate + (let ((elt (car undo-list))) + (not (and (consp elt) + (or (stringp (car elt)) + (integerp (car elt))))))) (setq undo-list (cdr undo-list))) ; get the last undo record (if (and (eq last-command 'undo) (or (eq pending-undo-list t) 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 3a24595e..e67a7774 100644 --- a/generic/proof-script.el +++ b/generic/proof-script.el @@ -1240,12 +1240,16 @@ activation is considered to have failed and an error is given." (assert (null proof-script-buffer) "Bug in proof-activate-scripting: deactivate failed.") - ;; Set the active scripting buffer, and initialise regions + ;; Set the active scripting buffer (setq proof-script-buffer (current-buffer)) ;; Fire up the prover (or check it's going the right way). - (proof-shell-ready-prover queuemode) + (condition-case-unless-debug err + (proof-shell-ready-prover queuemode) + (error (setq proof-script-buffer nil) + (signal (car err) (cdr err)))) + ;; Initialise regions (if (proof-locked-region-empty-p) ; leave alone if non-empty (proof-init-segmentation)) @@ -1985,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 4f89963e..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))) @@ -379,7 +392,10 @@ process command." (setq proof-shell-buffer (get-buffer (concat "*" proc "*"))) (unless (proof-shell-live-buffer) - ;; Give error now if shell buffer isn't live (process exited) + ;; Give error now if shell buffer isn't live (process exited). We also + ;; set the process filter to nil to avoid processing error messages + ;; related to the process exit. + (set-process-filter (get-buffer-process proof-shell-buffer) nil) (setq proof-shell-buffer nil) (error "Starting process: %s..failed" prog-command-line))) @@ -448,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) @@ -810,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 e4fe9096..48a2bdae 100644 --- a/generic/proof-site.el +++ b/generic/proof-site.el @@ -72,8 +72,8 @@ ;; (eval-and-compile -;; WARNING: do not edit next line (constant is edited in Makefile.devel) - (defconst proof-general-version "Proof General Version 4.3pre150313. Released by da." + ;; WARNING: do not edit next line (constant is edited in Makefile.devel) + (defconst proof-general-version "Proof General Version 4.4.1~pre." "Version string identifying Proof General release.")) (defconst proof-general-short-version @@ -82,7 +82,7 @@ (string-match "Version \\([^ ]+\\)\\." proof-general-version) (match-string 1 proof-general-version)))) -(defconst proof-general-version-year "2015") +(defconst proof-general-version-year "2016") ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; diff --git a/generic/proof-splash.el b/generic/proof-splash.el index 19516af4..25db0946 100644 --- a/generic/proof-splash.el +++ b/generic/proof-splash.el @@ -46,38 +46,35 @@ Proof General." (defcustom proof-splash-contents '(list - nil - (proof-get-image "pg-text" t) - nil - (proof-get-image "ProofGeneral-image") + (proof-get-image "ProofGeneral-splash.png") nil "Welcome to" (concat proof-assistant " Proof General!") nil (concat "Version " proof-general-short-version ".") nil - (concat "(C) LFCS, University of Edinburgh " proof-general-version-year) + (concat "© LFCS, University of Edinburgh & contributors " proof-general-version-year) nil nil :link '(" Read the " "Proof General documentation" - (lambda (button) (info "ProofGeneral"))) - :link '(" Please report problems at " - "Proof General trac" - (lambda (button) - (browse-url "http://proofgeneral.inf.ed.ac.uk/trac")) - "Report bugs at http://proofgeneral.inf.ed.ac.uk/trac") - :link '("Visit the " "Proof General wiki" - (lambda (button) - (browse-url "http://proofgeneral.inf.ed.ac.uk/wiki")) - "Write lots of helpful things at http://proofgeneral.inf.ed.ac.uk/wiki") + (lambda (button) (info "ProofGeneral"))) + :link '(" Please report problems on the " + "Github issue tracker" + (lambda (button) + (browse-url "https://github.com/ProofGeneral/PG/issues")) + "Report bugs at https://github.com/ProofGeneral/PG") + :link '("Visit the " "Proof General Github page" + (lambda (button) + (browse-url "https://github.com/ProofGeneral/PG")) + "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/") + (lambda (button) + (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))) + :link '("Find out about Emacs on the Help menu -- start with the " + "Emacs Tutorial" (lambda (button) (help-with-tutorial))) nil "See this screen again with Proof-General -> About" ) @@ -117,27 +114,12 @@ If it is nil, a new line is inserted." (and (listp img) (eq (car img) 'image))) -(defun proof-get-image (name &optional nojpeg default) - "Construct an image instantiator for an image, or string failing that. -Different formats are chosen from according to what can be displayed. -Unless NOJPEG is set, try jpeg first. Then try gif, then xpm. -Gif filename depends on colour depth of display. -DEFAULT gives return value in case image not valid." - (let ((jpg (vector 'jpeg :file - (concat proof-images-directory name ".jpg"))) - (gif (vector 'gif :file - (concat proof-images-directory ".gif"))) - img) - (cond - (window-system - (find-image - (list - (list :type 'jpeg - :file (concat proof-images-directory name ".jpg")) - (list :type 'gif - :file (concat proof-images-directory name ".gif"))))) - (t - (or default (concat "[ image " name " ]")))))) +(defun proof-get-image (name) + "Load a PNG image NAME, or string on TTYs." + (if (display-graphic-p) + (find-image + `((:type png :file ,(expand-file-name name proof-images-directory)))) + (concat "[ image " name " ]"))) (defvar proof-splash-timeout-conf nil "Holds timeout ID and previous window config for proof splash screen.") 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) |