From f424f6808ed1dc43830c2cc1ddbf380a3dc2d916 Mon Sep 17 00:00:00 2001
From: Thomas Kleymann
Date: Tue, 14 Oct 1997 09:29:17 +0000
Subject: proof-process-active-terminator is now an extension of
 proof-assert-until-point (it was broken and looks healthier now)

---
 proof.el | 30 +++++++++++++-----------------
 1 file changed, 13 insertions(+), 17 deletions(-)

diff --git a/proof.el b/proof.el
index 5408fead..b1c88d42 100644
--- a/proof.el
+++ b/proof.el
@@ -21,6 +21,10 @@
 ;;   beginning of the module? 
 
 ;; $Log$
+;; Revision 1.12  1997/10/14 09:29:17  tms
+;; proof-process-active-terminator is now an extension of
+;; proof-assert-until-point (it was broken and looks healthier now)
+;;
 ;; Revision 1.11  1997/10/13 17:09:52  tms
 ;; put script-management branch back on main branch
 ;;
@@ -1003,7 +1007,7 @@ at the end of locked region (after inserting a newline)."
 	(setq semis (cdr semis)))
     (nreverse alist)))
 
-(defun proof-assert-until-point ()
+(defun proof-assert-until-point (&optional unclosed-comment-hook)
   (interactive)
   (let ((pt  (point)) semis crowbar vanillas)
     (setq crowbar (proof-steal-process))
@@ -1012,7 +1016,9 @@ at the end of locked region (after inserting a newline)."
 	  (progn (goto-char pt)
 		 (error "Nothing to do!")))
       (setq semis (proof-segment-up-to (point)))
-      (if (eq 'unclosed-comment (car semis)) (setq semis (cdr semis)))
+      (if (eq 'unclosed-comment (car semis))
+	  (progn (run-hook unclosed-comment-hook)
+		 (setq semis (cdr semis))))
       (if (and (not crowbar) (null semis)) (error "Nothing to do!")))
     (goto-char (caddar semis))
     (setq vanillas (proof-semis-to-vanillas (nreverse semis)))
@@ -1147,30 +1153,20 @@ current command."
     (self-insert-command 1)))
 
 (defun proof-process-active-terminator ()
-  "Insert the terminator in an intelligent way and send the commands
-  between the previous and the new terminator to the proof process."
-  (proof-check-process-available)
+  "Insert the terminator in an intelligent way and assert until the new terminator."
   (let ((mrk (point)) ins semis)
     (if (looking-at "\\s-\\|\\'\\|\\w") 
 	(if (not (re-search-backward "\\S-" (proof-end-of-locked) t))
 	    (error "Nothing to do!")))
     (if (not (= (char-after (point)) proof-terminal-char))
 	(progn (forward-char) (insert proof-terminal-string) (setq ins t)))
-    (setq semis (proof-segment-up-to (point)))    
-    (if (null semis) (error "Nothing to do!"))
-    (if (eq 'unclosed-comment (car semis)) 
-	(progn (if ins (backward-delete-char 1))
-	       (goto-char mrk) (insert proof-terminal-string))
-      (goto-char (caddar (last semis)))
-      (proof-start-queue (proof-end-of-locked) (point)
-			 (proof-semis-to-vanillas semis)))))
-
-
+    (proof-assert-until-point
+     (function ()
+	       (if ins (backward-delete-char 1))
+	       (goto-char mrk) (insert proof-terminal-string)))))
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;; Proof mode configuration                                         ;;
-;; Eventually there will be some more                               ;;
-;; functionality here common to both coq and lego.                  ;;
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 
 
-- 
cgit v1.2.3