aboutsummaryrefslogtreecommitdiffhomepage
path: root/generic/pg-assoc.el
blob: 1a1dcd235239175967da26fbc12ce092e260ad8c (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
;;; pg-assoc.el --- Functions for associated buffers
;;
;; Copyright (C) 1994-2008 LFCS Edinburgh. 
;; Authors:   David Aspinall, Yves Bertot, Healfdene Goguen,
;;            Thomas Kleymann and Dilip Sequeira
;; License:   GPL (GNU GENERAL PUBLIC LICENSE)
;;
;; $Id$
;;
;;
;; Defines an empty mode inherited by modes of the associated buffers.
;;

;;; Code:

(eval-when-compile 
  (require 'proof-syntax)			; proof-replace-{string,regexp}
  (require 'span)				; spans
  (require 'cl))				; incf


(eval-and-compile ; defines proof-universal-keys-only-mode-map at compile time
  (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)))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;
;; Return a list of associated buffers
;;

;;;###autoload
(defun proof-associated-buffers ()
  "Return a list of the associated buffers.  
Some may be dead/nil."
  (list proof-goals-buffer
	proof-response-buffer
	proof-trace-buffer
	proof-thms-buffer))


;;;###autoload
(defun proof-associated-windows ()
  "Return a list of the associated buffers windows.  
Dead or nil buffers are not represented in the list."
  (let ((bufs (proof-associated-buffers))
	buf wins)
    (while bufs
      (setq buf (car bufs))
      (if (and buf (get-buffer-window buf))
	  (setq wins (cons (get-buffer-window buf) wins)))
      (setq bufs (cdr bufs)))
    wins))

(provide 'pg-assoc)
;;; pg-assoc.el ends here