Added some interface stuff:

 - an default coq abbrev file, loaded only if no abbrev table exists
   for coq;
 - some menu entries and shortcuts for abbrev;
 - a menu entry for "3 buffers view".

2 files changed, 112 insertions, 1 deletions

diff --git a/coq/coq-abbrev.el b/coq/coq-abbrev.el
new file mode 100644
index 00000000..bbfaae42
--- /dev/null
+++ b/coq/coq-abbrev.el
@@ -0,0 +1,64 @@
+;; default abbrev table
+
+(define-abbrev-table 'coq-mode-abbrev-table
+  '(
+    ("u" "unfold" nil 0)
+    ("si" "simpl" nil 0)
+    ("t" "trivial" nil 0)
+    ("dec" "decompose []" nil 0)
+    ("ab" "absurd" nil 0)
+    ("ao" "abstract omega" nil 0)
+    ("s" "simpl" nil 0)
+    ("r<" "rewrite <-" nil 0)
+    ("r" "rewrite" nil 0)
+    ("di" "discriminate" nil 0)
+    ("p" "Print" nil 0)
+    ("indv" "Inductive" nil 0)
+    ("o" "abstract omega" nil 0)
+    ("l" "Lemma  :" nil 0)
+    ("de" "Definition" nil 0)
+    ("awa" "auto with arith" nil 0)
+    ("i" "intro" nil 0)
+    ("h" "Hints  :" nil 0)
+    ("g" "generalize" nil 0)
+    ("co" "constructor" nil 0)
+    ("e" "elim" nil 0)
+    ("d" "Definition" nil 0)
+    ("c" "constructor" nil 0)
+    ("ge" "generalize" nil 0)
+    ("sym" "symmetry" nil 0)
+    ("a" "auto" nil 0)
+    ("re" "rewrite" nil 0)
+    ("eawa" "eauto with acthint" nil 0)
+    ("un" "unfold" nil 0)
+    ("eaw" "eauto with" nil 0)
+    ("fi" "functional induction" nil 0)
+    ("fs" "Functional Scheme xxx := Induction for yyy (opt:with ...)." nil 0)
+	 ("sc" "Scheme xxx := Induction for yyy Sort sss." nil 0)
+    ("sc" "Scheme" nil 0)
+    ("fi" "Fixpoint" nil 0)
+    ("eap" "eapply" nil 0)
+    ("ex" "exists" nil 0)
+    ("inv" "inversion" nil 0)
+    ("is" "intros" nil 0)
+    ("abs" "absurd" nil 0)
+    ("tr" "trivial" nil 0)
+    ("in" "intro" nil 0)
+    ("dis" "discriminate" nil 0)
+    ("aw" "auto with" nil 0)
+    ("pr" "Print" nil 0)
+    ("au" "auto" nil 0)
+    ("as" "assumption" nil 0)
+    ("sy" "symmetry" nil 0)
+    ("ar" "auto with arith" nil 0)
+    ("el" "elim" nil 0)
+    ("ap" "apply" nil 0)
+    ("gen" "generalize" nil 0)
+    ("hr" "Hint Resolve :" nil 0)
+    ("ind" "induction" nil 0)
+    ("fix" "Fixpoint  [] :  :=" nil 0)
+    ("sp" "simpl" nil 0)
+    ("re<" "rewrite <-" nil 0)
+    ("ea" "eauto" nil 0)
+    ("def" "Definition" nil 0)
+    ))
\ No newline at end of file
diff --git a/coq/coq.el b/coq/coq.el
index 8670a75e..2cb5fa53 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -84,7 +84,10 @@
 ;; ----- coq specific menu
 
 (defpgdefault menu-entries
-  '(["Print..." coq-Print t]
+  '(["expand abbrev at point" expand-abbrev t]
+    ["list abbrevs" list-abbrevs t]
+    ["3 buffers view" coq-three-b t]
+    ["Print..." coq-Print t]
     ["Check..." coq-Check t]
     ["Hints" coq-PrintHint t]
     ["Intros..." coq-Intros t]
@@ -507,6 +510,35 @@ 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)
+
+; This is arguable, but completion with a three key shortcut is bad, 
+; and the feault meta-/ is bad on some keyboards (especially french ones)
+(define-key global-map [(control backspace)] 'expand-abbrev)
+
+
+
+(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*")
+)
+
 
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
@@ -896,6 +928,21 @@ mouse activation."
                  ,(format "Check %s." thm))))))
   )
 
+
+;load the default coq abbrev file if no coq abbrev file is already read
+;TODO: add the holes and put holes in abbreviations.
+; This needs to add some code in generic/span*.el first, then add holes.el 
+; in the generaic part, and then ok.
+
+(if (and (boundp 'coq-mode-abbrev-table)
+         (not (equal coq-mode-abbrev-table (make-abbrev-table))))
+    (message "An abbrev table exists for coq, no default loaded")
+  (progn
+    (quietly-read-abbrev-file "coq-abbrev.el")
+    (message "coq default abbreviations loaded"))
+  )
+
+
 (provide 'coq)