Add proof-shell-strip-crs-from-output

3 files changed, 74 insertions, 0 deletions

diff --git a/generic/proof-compat.el b/generic/proof-compat.el
index dde429e1..10454cd3 100644
--- a/generic/proof-compat.el
+++ b/generic/proof-compat.el
@@ -60,6 +60,66 @@ that use a window system such as X, and false for text-only terminals."
       (or (eq (console-type) 'x)
 	  (eq (console-type) 'mswindows))))
 
+(or (fboundp 'replace-regexp-in-string)
+;; Code is taken from Emacs 21.1.1/subr.el 
+(defun replace-regexp-in-string (regexp rep string &optional
+					fixedcase literal subexp start)
+  "Replace all matches for REGEXP with REP in STRING.
+
+Return a new string containing the replacements.
+
+Optional arguments FIXEDCASE, LITERAL and SUBEXP are like the
+arguments with the same names of function `replace-match'.  If START
+is non-nil, start replacements at that index in STRING.
+
+REP is either a string used as the NEWTEXT arg of `replace-match' or a
+function.  If it is a function it is applied to each match to generate
+the replacement passed to `replace-match'; the match-data at this
+point are such that match 0 is the function's argument.
+
+To replace only the first match (if any), make REGEXP match up to \\'
+and replace a sub-expression, e.g.
+  (replace-regexp-in-string \"\\(foo\\).*\\'\" \"bar\" \" foo foo\" nil nil 1)
+    => \" bar foo\"
+"
+
+  ;; To avoid excessive consing from multiple matches in long strings,
+  ;; don't just call `replace-match' continually.  Walk down the
+  ;; string looking for matches of REGEXP and building up a (reversed)
+  ;; list MATCHES.  This comprises segments of STRING which weren't
+  ;; matched interspersed with replacements for segments that were.
+  ;; [For a `large' number of replacments it's more efficient to
+  ;; operate in a temporary buffer; we can't tell from the function's
+  ;; args whether to choose the buffer-based implementation, though it
+  ;; might be reasonable to do so for long enough STRING.]
+  (let ((l (length string))
+	(start (or start 0))
+	matches str mb me)
+    (save-match-data
+      (while (and (< start l) (string-match regexp string start))
+	(setq mb (match-beginning 0)
+	      me (match-end 0))
+	;; If we matched the empty string, make sure we advance by one char
+	(when (= me mb) (setq me (min l (1+ mb))))
+	;; Generate a replacement for the matched substring.
+	;; Operate only on the substring to minimize string consing.
+	;; Set up match data for the substring for replacement;
+	;; presumably this is likely to be faster than munging the
+	;; match data directly in Lisp.
+	(string-match regexp (setq str (substring string mb me)))
+	(setq matches
+	      (cons (replace-match (if (stringp rep)
+				       rep
+				     (funcall rep (match-string 0 str)))
+				   fixedcase literal str subexp)
+		    (cons (substring string start mb) ; unmatched prefix
+			  matches)))
+	(setq start me))
+      ;; Reconstruct a string from the pieces.
+      (setq matches (cons (substring string start l) matches)) ; leftover
+      (apply #'concat (nreverse matches))))))
+
+
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;;;
diff --git a/generic/proof-config.el b/generic/proof-config.el
index 61820697..ee8015d6 100644
--- a/generic/proof-config.el
+++ b/generic/proof-config.el
@@ -1996,6 +1996,12 @@ up the display (or even worse, the synchronization)."
   :type 'boolean
   :group 'proof-shell)
   
+(defcustom proof-shell-strip-crs-from-output t ;; proof-running-on-win32
+  "If non-nil, remove carriage returns (^M) at the end of lines from output.
+This is enabled for Win32 systems by default."
+  :type 'boolean
+  :group 'proof-shell)
+
 (defcustom proof-shell-insert-hook nil 
   "Hooks run by proof-shell-insert before inserting a command.
 Can be used to configure the proof assistant to the interface in
diff --git a/generic/proof-shell.el b/generic/proof-shell.el
index f1268ca3..30d1a68a 100644
--- a/generic/proof-shell.el
+++ b/generic/proof-shell.el
@@ -1380,6 +1380,14 @@ correspond with initializing the process.  The
 ordinary output before the first prompt is ignored (urgent messages, 
 however, are always processed; hence their name)."
   (save-excursion
+    ;; Strip CRs.
+    (if proof-shell-strip-crs-from-output
+	(progn
+	  (setq str (replace-regexp-in-string "\r+$" "" str))
+	  ;; Do the same thing in the buffer via comint's function
+	  ;; (sometimes put on comint-output-filter-functions too).
+	  (comint-strip-ctrl-m)))
+
     ;; Process urgent messages.
     (and proof-shell-eager-annotation-start
 	 (proof-shell-process-urgent-messages))