aboutsummaryrefslogtreecommitdiffhomepage
path: root/coq
diff options
context:
space:
mode:
authorGravatar David Aspinall <da@inf.ed.ac.uk>2004-04-02 16:59:24 +0000
committerGravatar David Aspinall <da@inf.ed.ac.uk>2004-04-02 16:59:24 +0000
commit2a8f91fc3c959ff96a583326815b57e54d262e90 (patch)
treebcf5e371d7147329035a54f3d24841f3fdeb3c64 /coq
parent2a5709c354e09b06556f3f1e19bf2d9a5ad91564 (diff)
Remove three-buffer stuff (made generic)
Diffstat (limited to 'coq')
-rw-r--r--coq/coq.el47
1 files changed, 14 insertions, 33 deletions
diff --git a/coq/coq.el b/coq/coq.el
index f8f3beff..b6e104c1 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -476,7 +476,11 @@ This is specific to coq-mode."
(define-key coq-keymap [(control ?p)] 'coq-Print)
(define-key coq-keymap [(control ?c)] 'coq-Check)
(define-key coq-keymap [(control ?h)] 'coq-PrintHint)
-(define-key coq-keymap [(control f3)] 'coq-three-b)
+;; da: I've moved this three buffer layout into the main code now,
+;; making it default for three bufer mode. The function
+;; `proof-layout-windows' lays out according to current display
+;; mode: you can use this (C-c C-l) to do what binding below did.
+;;(define-key coq-keymap [(control f3)] 'coq-three-b)
; This is arguable, but completion with a three key shortcut is bad,
; and the feault meta-/ is bad on some keyboards (especially french ones)
@@ -484,29 +488,6 @@ This is specific to coq-mode."
-(defun three-b (b1 b2 b3)
- "Select three buffers.
- Put them into three windows, selecting the last one."
- (interactive "bBuffer1:\nbBuffer2:\nbBuffer3:")
- (delete-other-windows)
- (split-window-horizontally)
- (switch-to-buffer b1)
- (other-window 1)
- (split-window-vertically)
- (switch-to-buffer b2)
- (other-window 1)
- (switch-to-buffer b3)
- (other-window 1)
-)
-
-(defun coq-three-b ()
- (interactive)
- (three-b (buffer-name (first (buffer-list)))
- "*coq-response*" "*coq-goals*")
-)
-
-
-
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; Indentation ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
@@ -841,15 +822,15 @@ This is specific to coq-mode."
"Whether to automatically compile vos and track dependencies."
:type 'boolean
:eval (if coq-auto-compile-vos
- (setq proof-shell-inform-file-processed-cmd
- coq-proof-shell-inform-file-processed-cmd
- proof-shell-process-file
- coq-proof-shell-process-file
- proof-shell-inform-file-retracted-cmd
- coq-proof-shell-inform-file-retracted-cmd)
- (setq proof-shell-inform-file-processed-cmd nil
- proof-shell-process-file nil
- proof-shell-inform-file-retracted-cmd nil)))
+ (setq proof-shell-inform-file-processed-cmd
+ coq-proof-shell-inform-file-processed-cmd
+ proof-shell-process-file
+ coq-proof-shell-process-file
+ proof-shell-inform-file-retracted-cmd
+ coq-proof-shell-inform-file-retracted-cmd)
+ (setq proof-shell-inform-file-processed-cmd nil
+ proof-shell-process-file nil
+ proof-shell-inform-file-retracted-cmd nil)))
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;