Temporary fix for problem with Emacs 20.5 reported by Pierre

1 files changed, 21 insertions, 52 deletions

diff --git a/generic/proof-shell.el b/generic/proof-shell.el
index bcb1d4a6..26b946c2 100644
--- a/generic/proof-shell.el
+++ b/generic/proof-shell.el
@@ -80,29 +80,13 @@ See the functions `proof-start-queue' and `proof-exec-loop'.")
 ;; code is single-threaded, a loop parsing process output cannot get
 ;; pre-empted by the user trying to send more input to the process,
 ;; or by the process filter trying to deal with more output.
+;; (Moreover, we can tell when the process is busy because the 
+;; queue is non-empty).
 ;;
 ;;
 
 ;;
-;; History of these horrible functions.
-;;
-;;  proof-check-process-available
-;;    Checks whether the proof process is available.
-;; Specifically:
-;;     (1) Is a proof process running?
-;;     (2) Is the proof process idle?
-;;     (3) Does the current buffer own the proof process?
-;;     (4) Is the current buffer a proof script?
-;; It signals an error if at least one of the conditions is not
-;; fulfilled. If optional arg RELAXED is set, only (1) and (2) are 
-;; tested.
-;;
-;; Later, proof-check-process-available was altered to also
-;; start a proof shell if necessary, although this is also
-;; done (later?) in proof-grab-lock.  It was also altered to
-;; perform configuration for switching scripting buffers.
-;;
-;; Now, we have two functions again:
+;; We have two functions:
 ;;
 ;;  proof-shell-ready-prover   
 ;;    starts proof shell, gives error if it's busy.
@@ -116,28 +100,8 @@ See the functions `proof-start-queue' and `proof-exec-loop'.")
 ;;  proof-shell-available
 ;;    returns non-nil if a proof shell is active and not locked.
 ;;
-;; Maybe proof-shell-ready-prover doesn't need to start the shell,
-;; we can find that out later.
-;;
-;; Chasing down 'relaxed' flags:
-;;
-;;   was passed into proof-grab by proof-start-queue
-;;    only call to proof-start-queue with this arg is in
-;;    proof-shell-invisible-command.
-;;   only call of proof-shell-invisible-command with relaxed arg
-;;   is in proof-minibuffer-cmd.
-;;  --- presumably so that command could be executed from any
-;;  buffer, not just a scripting one?
+;; Maybe proof-shell-ready-prover doesn't need to start the shell?
 ;;
-;;  I think it's wrong for proof-shell-invisible-command to enforce
-;;  scripting buffer!
-;; 
-;;  This is reflected now by just calling (proof-shell-ready-prover)
-;;  in proof-shell-invisible-command, not proof-check-process-available.
-;;
-;; Hopefully we can get rid of these messy 'relaxed' flags now.
-;;
-;;  -da.
 
 (defun proof-shell-ready-prover (&optional queuemode)
   "Make sure the proof assistant is ready for a command.
@@ -235,14 +199,13 @@ Does nothing if proof assistant is already running."
     ;;		  (+ 1 (aref proc (- (length proc) 2))))
     ;;	  (setq proc (concat proc "<2>"))))
 
-    ;; da: Finally removed this because it leads to objectionable 
-    ;; proliferation of buffers when startup fails.
-
-     ;; (while (get-buffer (concat "*" proc "*"))
-     ;; (if (string= (substring proc -1) ">")
-     ;; (aset proc (- (length proc) 2) 
-     ;; (+ 1 (aref proc (- (length proc) 2))))
-     ;; (setq proc (concat proc "<2>"))))
+      ;; da: Finally removed this because it leads to objectionable 
+      ;; proliferation of buffers when startup fails.
+      ;; (while (get-buffer (concat "*" proc "*"))
+      ;; (if (string= (substring proc -1) ">")
+      ;; (aset proc (- (length proc) 2) 
+      ;; (+ 1 (aref proc (- (length proc) 2))))
+      ;; (setq proc (concat proc "<2>"))))
       
       (message (format "Starting process: %s" proof-prog-name))
 
@@ -262,7 +225,8 @@ Does nothing if proof assistant is already running."
 	    ;; Experimental fix for backslash/long line problem.  
 	    ;; Make start-process (called by make-comint)
 	    ;; use a pipe, not a pty.  Seems to work.
-	    (process-connection-type nil))
+	    ; (process-connection-type nil))
+	    )
 
 	;; An improvement here might be to catch failure of
 	;; make-comint and then kill off the buffer.  Then we 
@@ -1527,12 +1491,17 @@ however, are always processed; hence their name)."
 
     (if ;; Some proof systems can be hacked to have annotated prompts;
 	;; for these we set proof-shell-wakeup-char to the annotation 
-	;; special.  
+	;; special, and look for it in the output before doing anything.
 	(if proof-shell-wakeup-char
 	    ;; FIXME: this match doesn't work in emacs-mule, darn.
 	    ;; (string-match (char-to-string proof-shell-wakeup-char) str))
-	    (find proof-shell-wakeup-char str)
-	  ;; Others may rely on a standard top-level (e.g. SML) whose
+	    ;; FIXME: this match doesn't work in FSF emacs 20.5, darn.
+	    ;; (find proof-shell-wakeup-char str)
+	    ;; FIXME: 3.1pre: temporarily, use both tests!
+	    (or
+	     (string-match (char-to-string proof-shell-wakeup-char) str)
+	     (find proof-shell-wakeup-char str))
+	  ;; Others systems rely on a standard top-level (e.g. SML) whose
 	  ;; prompts may be difficult or impossible to hack.
 	  ;; For those we must search in the buffer for the prompt.
 	  t)