added proof-find-end-of-command

moved some bindings from lego-mode-map to proof-mode-map

2 files changed, 44 insertions, 8 deletions

diff --git a/lego.el b/lego.el
index f976b7a2..b81a4449 100644
--- a/lego.el
+++ b/lego.el
@@ -3,7 +3,7 @@
 ;; rearranging Thomas Schreiber's code.
 
 ;; Maintainer: LEGO Team <lego@dcs.ed.ac.uk>
-;; Time-stamp: <17 Oct 96 djs /home/lego/emacs/lego.el>
+;; Time-stamp: <25 Oct 96 tms ~/elisp/lego.el>
 ;; Thanks to David Aspinall, Robert Boyer, Rod Burstall,
 ;;           James McKinna, Mark Ruys, Martin Steffen, Perdita Stevens  
 
@@ -533,13 +533,16 @@ nicked from AUCTeX's tex-buffer.el"
 ;; keymaps and menus
 
   (lego-add-common-bindings lego-mode-map)
-  (define-key lego-mode-map ";"        'proof-active-terminator)
+
+  ;; tms - I don't understand why "(control c) ?;" works, yet
+  ;; "(control c) proof-terminal-char" doesn't 
+  (define-key lego-mode-map [(control c) ?;]
+  'proof-active-terminator-minor-mode)
+  (define-key lego-mode-map proof-terminal-char       'proof-active-terminator)
+
   (define-key lego-mode-map [(control c) (control b)] 'lego-make-buffer)
   (define-key lego-mode-map [(control c) (control h)] 
     'lego-make-buffer-until-point)
-  (define-key lego-mode-map "\C-c;"    'proof-active-terminator-minor-mode)
-  (define-key lego-mode-map [(control c) (control j)] 'proof-send-line)
-  (define-key lego-mode-map [(control c) (control r)] 'proof-send-region)
 
   (easy-menu-add lego-mode-menu lego-mode-map)
 
diff --git a/proof.el b/proof.el
index e28bd595..0797c9d9 100644
--- a/proof.el
+++ b/proof.el
@@ -3,7 +3,7 @@
 ;; rearranging Thomas Schreiber's code.
 
 ;; Maintainer: LEGO Team <lego@dcs.ed.ac.uk>
-;; Time-stamp: <17 Oct 96 djs /home/lego/emacs/lego.el>
+;; Time-stamp: <25 Oct 96 tms ~/elisp/proof.el>
 ;; Thanks to David Aspinall, Robert Boyer, Rod Burstall,
 ;;           James McKinna, Mark Ruys, Martin Steffen, Perdita Stevens  
 
@@ -141,6 +141,16 @@
   (concat (substring address 0 (match-end 0))
           (file-name-directory (substring address (match-end 0)))))
 
+(defun occurence (STRING &optional LOWER-BOUND UPPER-BOUND)
+  "Counts the number of occurences of STRING in the current buffer
+   between the positions LOWER-BOUND and UPPER-BOUND.
+   Optional first argument. nil is equivalent to (point-min).
+   Optional second argument. nil is equivalent to (point-max)."
+  (save-excursion
+    (let ((LOWER-BOUND (or LOWER-BOUND (point-min))))
+      (goto-char LOWER-BOUND)
+      (let ((pos (search-forward STRING UPPER-BOUND t)))
+	(if pos (+ 1 (occurence STRING pos UPPER-BOUND)) 0)))))
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;;          A few random hacks                                      ;;
@@ -169,6 +179,25 @@
      (goto-char (point-min))
      (proof-skip-comments)))
 
+
+;; there seems to be some duplication of work here, as one might
+;; expect that the functionality of proof-find-end-of-command would be
+;; required in proof-process-active-terminator
+(defun proof-find-end-of-command (&optional COUNT)
+  "Move to the end of the command. COUNT-1 end-of-command symbols
+  `proof-terminal-string' are within comments"
+  (interactive)
+  (let ((point (point))
+	(pos   (search-forward proof-terminal-string nil nil COUNT)))
+    (and pos
+ 	;; an end of command has been found
+	;; is pos within a comment relative to the starting point of
+	;; the search?
+	 (> (occurence proof-comment-start point (point))
+	    (occurence proof-comment-end   point (point)))
+	 (goto-char point)
+	 (proof-find-end-of-command (if COUNT (+ 1 COUNT) 2)))))
+
 (defun proof-shell-buffer () (get-buffer proof-shell-buffer-name))
 
 (defun proof-display-buffer (buffer)
@@ -446,8 +475,8 @@ current command."
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;; Proof mode configuration                                         ;;
-;; Eventually there will be some functionality here common to both  ;;
-;; coq and lego. But for the moment, they're just mode shells.      ;;
+;; Eventually there will be some more                               ;;
+;; functionality here common to both coq and lego.                  ;;
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 
 
@@ -455,6 +484,10 @@ current command."
   "Proof" "Proof mode - not standalone"
   ())
 
+(define-key proof-mode-map [(control c) (control e)]
+  'proof-find-end-of-command)
+(define-key proof-mode-map [(control c) (control j)] 'proof-send-line)
+(define-key proof-mode-map [(control c) (control r)] 'proof-send-region)
 
 (define-derived-mode proof-shell-mode comint-mode 
   "proof-shell" "Proof shell mode - not standalone"