Added proof-assistant-keymap and commands for defining insert keys.

1 files changed, 9 insertions, 25 deletions

diff --git a/coq/coq.el b/coq/coq.el
index 14be4ab6..3d99ba68 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -283,18 +283,6 @@
 ;;   Commands specific to coq                                       ;;
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 
-(defun coq-Intros () 
-  "Shortcut for Intros.
-This is specific to coq-mode." 
-  (interactive) 
-  (insert "Intros "))
-
-(defun coq-Apply () 
-  "Shortcut for Apply
-This is specific to coq-mode."  
-  (interactive) 
-  (insert "Apply "))
-
 (defun coq-SearchIsos ()
   "Search a term whose type is isomorphic to given type
 This is specific to coq-mode."
@@ -305,11 +293,6 @@ This is specific to coq-mode."
     (proof-shell-invisible-command
      (concat "SearchIsos " cmd proof-terminal-string))))
 
-(defun coq-begin-Section ()
-  "begins a Coq section."
-  (interactive)
-  (insert "Section "))
-
 (defun coq-end-Section ()
   "Ends a Coq section."
   (interactive)
@@ -335,6 +318,15 @@ This is specific to coq-mode."
 	 (l (string-match ".v" n)))
     (compile (concat "make " (substring n 0 l) ".vo"))))
 
+(proof-defshortcut coq-Intros        "Intros "  ?i)
+(proof-defshortcut coq-Apply         "Apply "   ?a)
+(proof-defshortcut coq-begin-Section "Section " ?s)
+
+(define-key proof-assistant-keymap ?e 'coq-end-Section)
+(define-key proof-assistant-keymap ?m 'coq-Compile)
+(define-key proof-assistant-keymap ?o 'coq-SearchIsos)
+
+
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;;   Indentation                                                    ;;
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
@@ -472,14 +464,6 @@ This is specific to coq-mode."
   
   (proof-config-done)
 
-;; Coq-specific key mappings
-
-  (define-key (current-local-map) [(control c) ?I] 'coq-Intros)
-  (define-key (current-local-map) [(control c) ?a] 'coq-Apply)
-  (define-key (current-local-map) [(control c) ?s] 'coq-begin-Section)
-  (define-key (current-local-map) [(control c) ?e] 'coq-end-Section)
-  (define-key (current-local-map) [(control c) (control m)] 'coq-Compile)
-
 ;; outline
   
   (make-local-variable 'outline-regexp)