Refactoring

1 files changed, 105 insertions, 0 deletions

diff --git a/generic/pg-response.el b/generic/pg-response.el
new file mode 100644
index 00000000..86dfe0ea
--- /dev/null
+++ b/generic/pg-response.el
@@ -0,0 +1,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.