blob: 86dfe0ea59bc78e3ed432fb6c1191f16021f0e97 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
|
;; pg-response.el Proof General response buffer mode.
;;
;; Copyright (C) 1994-2002 LFCS Edinburgh.
;; Authors: David Aspinall, Healfdene Goguen,
;; Thomas Kleymann and Dilip Sequeira
;; License: GPL (GNU GENERAL PUBLIC LICENSE)
;;
;; $Id$
;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;
;; Response buffer mode
;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(eval-and-compile
(define-derived-mode proof-universal-keys-only-mode fundamental-mode
proof-general-name "Universal keymaps only"
;; Doesn't seem to supress TAB, RET
(suppress-keymap proof-universal-keys-only-mode-map 'all)
(proof-define-keys proof-universal-keys-only-mode-map
proof-universal-keys)))
(eval-and-compile
(define-derived-mode proof-response-mode proof-universal-keys-only-mode
"PGResp" "Responses from Proof Assistant"
(setq proof-buffer-type 'response)
(define-key proof-response-mode-map [q] 'bury-buffer)
(easy-menu-add proof-response-mode-menu proof-response-mode-map)
(easy-menu-add proof-assistant-menu proof-response-mode-map)
(proof-toolbar-setup)
(setq proof-shell-next-error nil) ; all error msgs lost!
(erase-buffer)))
(easy-menu-define proof-response-mode-menu
proof-response-mode-map
"Menu for Proof General response buffer."
(cons proof-general-name
(append
proof-toolbar-scripting-menu
proof-shared-menu
proof-config-menu
proof-bug-report-menu)))
(defun proof-response-config-done ()
"Complete initialisation of a response-mode derived buffer."
(proof-font-lock-configure-defaults nil)
(proof-x-symbol-configure))
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;
;; Multiple frames for goals and response buffers
;;
;; -- because who's going to bother do this by hand?
;;
(defvar proof-shell-special-display-regexp nil
"Regexp for special-display-regexps for multiple frame use.
Internal variable, setting this will have no effect!")
(defun proof-multiple-frames-enable ()
(cond
(proof-multiple-frames-enable
(setq special-display-regexps
(union special-display-regexps
(list proof-shell-special-display-regexp)))
;; If we're on XEmacs with toolbar, turn off toolbar and
;; menubar for the small frames to save space.
;; FIXME: this could be implemented more smoothly
;; with property lists, and specifiers should perhaps be set
;; for the frame rather than the buffer. Then could disable
;; minibuffer, too.
;; FIXME: add GNU Emacs version here.
(if (featurep 'toolbar)
(proof-map-buffers
(list proof-response-buffer proof-goals-buffer proof-trace-buffer)
(set-specifier default-toolbar-visible-p nil (current-buffer))
;; (set-specifier minibuffer (minibuffer-window) (current-buffer))
(set-specifier has-modeline-p nil (current-buffer))
(set-specifier menubar-visible-p nil (current-buffer))
;; gutter controls buffer tab visibility in XE 21.4
(and (boundp 'default-gutter-visible-p)
(set-specifier default-gutter-visible-p nil (current-buffer)))))
;; Try to trigger re-display of goals/response buffers,
;; on next interaction.
;; FIXME: would be nice to do the re-display here, rather
;; than waiting for next re-display
(delete-other-windows
(if proof-script-buffer
(get-buffer-window proof-script-buffer t))))
(t
;; FIXME: would be nice to kill off frames automatically,
;; but let's leave it to the user for now.
(setq special-display-regexps
(delete proof-shell-special-display-regexp
special-display-regexps)))))
(provide 'pg-response)
;; pg-response.el ends here.
|
