From e6d5b8b8b19ae60f76f34563b0a8eca4fb89e6e2 Mon Sep 17 00:00:00 2001 From: David Aspinall Date: Tue, 2 May 2000 12:05:41 +0000 Subject: Added proof-assistant-keymap and commands for defining insert keys. --- lego/lego.el | 21 +++------------------ 1 file changed, 3 insertions(+), 18 deletions(-) (limited to 'lego/lego.el') diff --git a/lego/lego.el b/lego/lego.el index 24e1a63e..26b869cb 100644 --- a/lego/lego.el +++ b/lego/lego.el @@ -277,20 +277,9 @@ Given is the first SPAN which needs to be undone." ;; Commands specific to lego ;; ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -(defun lego-intros () - "intros." - (interactive) - (insert "intros ")) - -(defun lego-Intros () - "insert Intros." - (interactive) - (insert "Intros ")) - -(defun lego-Refine () - "Insert Refine." - (interactive) - (insert "Refine ")) +(proof-defshortcut lego-Intros "Intros " ?I) +(proof-defshortcut lego-intros "intros " ?i) +(proof-defshortcut lego-Refine "Refine " ?r) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; Lego Indentation ;; @@ -397,10 +386,6 @@ Checks the width in the `proof-goals-buffer'" (proof-config-done) - (define-key (current-local-map) [(control c) ?i] 'lego-intros) - (define-key (current-local-map) [(control c) ?I] 'lego-Intros) - (define-key (current-local-map) [(control c) ?r] 'lego-Refine) - ;; outline (make-local-variable 'outline-regexp) -- cgit v1.2.3