Fix so that buffer names are shorter (esp for Coq).

A fixed version of Patrick's earlier patch.

1 files changed, 6 insertions, 10 deletions

diff --git a/generic/proof-shell.el b/generic/proof-shell.el
index fdfb9af7..3571b1d1 100644
--- a/generic/proof-shell.el
+++ b/generic/proof-shell.el
@@ -209,20 +209,16 @@ Does nothing if proof assistant is already running."
 	  (setq proof-prog-name (read-shell-command "Run process: "
 						    proof-prog-name))))
     (let ((proc
+	   ;; "Inferior" is Emacs terminology for sub-shell processes.
 	   (concat "Inferior "
+		   ;; Try to pick useful part of command name
+		   ;;  -- basename component of command less arguments
 		   (substring proof-prog-name
-			      (string-match "[^/]*$" proof-prog-name)))))
-         ; da: this change by patrl introduces a bug with 
-         ; Isabelle (& others?), where proof-prog-name is simply "isabelle".  
-         ; The first match returns nil instead of 0.
-         ;((proc
-	 ;  (concat "Inferior "
-	 ;	   (substring proof-prog-name
-	 ;		       (string-match "[^ /]* " proof-prog-name)
-	 ;		       (string-match  " " proof-prog-name)))))
+			      (or (string-match "[^/]*[ ]" proof-prog-name) 0)
+			      (string-match " " proof-prog-name)))))
     ;; FIXME da: We don't really need this.  We never have more than
     ;; one proof shell running at a time.  We might as well
-    ;; kill off the old buffer anyway.  But leave it in in case of
+    ;; kill off the old buffer anyway.  But leave it in for now for
     ;; future expansion, or for user to inspect the old buffer.
       (while (get-buffer (concat "*" proc "*"))
 	(if (string= (substring proc -1) ">")