aboutsummaryrefslogtreecommitdiffhomepage
path: root/generic/pg-response.el
diff options
context:
space:
mode:
Diffstat (limited to 'generic/pg-response.el')
-rw-r--r--generic/pg-response.el49
1 files changed, 28 insertions, 21 deletions
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))))))