Patch for synchronization problem in Coq, perhaps others.

2 files changed, 48 insertions, 30 deletions

diff --git a/generic/proof-config.el b/generic/proof-config.el
index 10b539a7..302852dc 100644
--- a/generic/proof-config.el
+++ b/generic/proof-config.el
@@ -29,7 +29,7 @@
 ;;  6. Goals buffer configuration
 ;;  7. Splash screen settings
 ;;  8. X-Symbol support
-;;  9. Prover specific settings
+;;  9. Prover specific settings [NEW in 3.2 -- using new mechanism]
 ;; 10. Global constants 
 ;;
 ;; The user options don't need to be set on a per-prover basis,
@@ -1169,19 +1169,28 @@ group.  This allows different proof assistants to coexist
   :type 'string
   :group 'proof-shell)
 
-;;
-;; FIXME: perhaps we should have pre-sync-init and 
-;; post-sync-init commands? 
-;;
+(defcustom proof-shell-pre-sync-init-cmd nil
+   "The command for configuring the proof process to gain synchronization.
+This command is sent before Proof General's synchronization
+mechanism is engaged, to allow customization inside the process
+to help gain syncrhonization (e.g. engaging special markup).
+
+It is better to configure the proof assistant for this purpose
+via command line options if possible, in which case this variable 
+does not need to be set.
+
+See also `proof-shell-init-cmd'."
+   :type '(choice string (const nil))
+   :group 'proof-shell)
+
 (defcustom proof-shell-init-cmd ""
    "The command for initially configuring the proof process.
-This command is sent to the process as soon as it starts up,
-perhaps in order to configure it for Proof General or to
-print a welcome message.
-Note that it is sent before Proof General's synchronization
-mechanism is engaged (in case the command engages it).  It
-is better to configure the proof assistant via command
-line options if possible."
+This command is sent to the process as soon as syncrhonization is gained
+(when an annotated prompt is first recognized).  It can be used to configure 
+the proof assistant in some way, or print a welcome message
+(since output before the first prompt is discarded).
+
+See also `proof-shell-pre-sync-init-cmd'."
    :type '(choice string (const nil))
    :group 'proof-shell)
 
@@ -1818,7 +1827,6 @@ Proof General."
 	       (match-end 0))
     nil
     "(C) LFCS, University of Edinburgh, 2000."
-    "D. Aspinall, H. Goguen, T. Kleymann, D. Sequiera"
     nil
     nil
 "    Please send problems and suggestions to proofgen@dcs.ed.ac.uk, 
@@ -1989,13 +1997,13 @@ for prover specific settings."
 
 (proof-defasscustom menu-entries nil
   "Extra entries for proof assistant specific menu. 
-A list of menu items [NAME CALLBACK ...].  See the documentation
+A list of menu items [NAME CALLBACK ENABLER ...].  See the documentation
 of `easy-menu-define' for more details."
   :type 'sexp)
 
 (proof-defasscustom help-menu-entries nil
   "Extra entries for help submenu for proof assistant specific help menu.
-A list of menu items [NAME CALLBACK ...].  See the documentation
+A list of menu items [NAME CALLBACK ENABLER ...].  See the documentation
 of `easy-menu-define' for more details."
   :type 'sexp)
 
diff --git a/generic/proof-shell.el b/generic/proof-shell.el
index 2452d78d..8cd93f17 100644
--- a/generic/proof-shell.el
+++ b/generic/proof-shell.el
@@ -1043,11 +1043,12 @@ proof-shell-exec-loop, to process the next item."
 
     (insert string)
 
-    ;; Advance the proof-marker.  This means that any output received
-    ;; up til now but not processed by the proof-shell-filter will be
-    ;; lost!  We must be careful to synchronize with the process
-    ;; before using proof-shell-insert.
-    (set-marker proof-marker (point))
+    ;; Advance the proof-marker, if synchronization has been gained.
+    ;; A null marker position indicates that synchronization is not
+    ;; yet gained.  (NB: Any output received before syncrhonization is
+    ;; gained is ignored!)
+    (unless (null (marker-position proof-marker))
+      (set-marker proof-marker (point)))
 
     ;; FIXME: possible improvement.  Make for post 3.0 releases
     ;; in case of problems.
@@ -1449,7 +1450,8 @@ This is a subroutine of proof-shell-filter."
   (let ((pt (point)) (end t) lastend start)
     (goto-char (marker-position proof-shell-urgent-message-scanner))
     (while (and end
-		(re-search-forward proof-shell-eager-annotation-start nil 'end))
+		(re-search-forward proof-shell-eager-annotation-start 
+				   nil 'end))
       (setq start (match-beginning 0))
       (if (setq end
 		(re-search-forward proof-shell-eager-annotation-end nil t))
@@ -1580,7 +1582,9 @@ however, are always processed; hence their name)."
 		  (progn
 		    (set-marker proof-marker (point))
 		    ;; The first time a prompt is seen we ignore any 
-		    ;; output that occured before it.  Process the
+		    ;; output that occured before it, assuming that
+		    ;; corresponds to uninteresting startup messages. 
+		    ;; We process the
 		    ;; action list to remove the first item if need
 		    ;; be (proof-shell-init-cmd sent if 
 		    ;; proof-shell-config-done).
@@ -1623,11 +1627,11 @@ however, are always processed; hence their name)."
 		     proof-shell-annotated-prompt-regexp nil t)
 		    (progn
 		      (backward-char (- (match-end 0) (match-beginning 0)))
-		      ;; FIXME: decoding x-symbols here is perhaps a bit 
+		      ;; NB: decoding x-symbols here is perhaps a bit 
 		      ;;  expensive; moreover it leads to problems 
 		      ;;  processing special characters as annotations
 		      ;;  later on.  So no fontify or decode.
-		      ;; (proof-fontify-region startpos (point))
+		      ;;   (proof-fontify-region startpos (point))
 		      (setq string (buffer-substring startpos (point)))
 		      (goto-char (point-max))	
 		      (proof-shell-filter-process-output string))))
@@ -1883,13 +1887,19 @@ processing."
       (add-hook 'kill-buffer-hook 'proof-shell-kill-function t t)
       (set-process-sentinel proc 'proof-shell-bail-out)
 
-      ;; Flush pending output from startup 
-      ;; (it gets hidden from the user)
-      (accept-process-output proc 1)
+      ;; Pre-sync initialization command.  This is necessary
+      ;; for proof assistants which change their output modes
+      ;; only after some initializations.
+      (if proof-shell-pre-sync-init-cmd
+	  (proof-shell-insert proof-shell-pre-sync-init-cmd 'init-cmd))
 
-      ;; Send intitialization command and wait for it to be
-      ;; processed.   Also ensure that proof-action-list is
-      ;; initialised. 
+      ;; Flush pending output from startup (it gets hidden from the user)
+      ;; while waiting for the prompt to appear
+      (while (null (marker-position proof-marker))
+	(accept-process-output proc 1))
+
+      ;; Send main intitialization command and wait for it to be
+      ;; processed.   Also ensure that proof-action-list is initialised. 
       (setq proof-action-list nil)
       (if proof-shell-init-cmd
 	  (proof-shell-invisible-command proof-shell-init-cmd t))