From 6f484df4fd4855b3a5ebd1537ccc2eefe315e9ed Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Thu, 28 Sep 2000 09:18:23 +0000
Subject: Added proof-shell-strip-crs-from-input, and unadvertised
 proof-script-fly-past-comments

---
 generic/proof-config.el | 16 +++++++++++++++-
 1 file changed, 15 insertions(+), 1 deletion(-)

diff --git a/generic/proof-config.el b/generic/proof-config.el
index dfcfecdf..3e4e6709 100644
--- a/generic/proof-config.el
+++ b/generic/proof-config.el
@@ -827,7 +827,7 @@ or `proof-script-parse-function'."
   :group 'prover-config)
 
 
-(defcustom proof-script-use-new-parsing nil
+(defcustom proof-script-use-new-parser nil
   "Whether to use the new parsing mechanism, based on `proof-script-parse-function'.
 This is a stop-gap option in Proof General 3.2 added because
 the parsing functions went through several iterations and the final
@@ -835,6 +835,12 @@ the parsing functions went through several iterations and the final
   :type 'boolean
   :group 'prover-config)
 
+;; Unadvertised customization variable
+(defvar proof-script-fly-past-comments t
+  "*If non-nil, fly past comments when scripting, coalescing them into single spans.")
+
+
+
 (defcustom proof-script-parse-function nil
   "A function which parses a portion of the proof script.
 It is called with the proof script as the current buffer, and
@@ -1857,6 +1863,14 @@ So we select pipes by default if it seems like we're on Solaris.
 We do not force pipes everywhere because this risks loss of data."
   :type 'boolean
   :group 'proof-shell)
+
+(defcustom proof-shell-strip-crs-from-input t
+  "If non-nil, replace carriage returns in every input with spaces.
+This is enabled by default: it is appropriate for some systems
+because several CR's can result in several prompts, which may mess
+up the display (or even worse, the synchronization)."
+  :type 'boolean
+  :group 'proof-shell)
   
 (defcustom proof-shell-insert-hook nil 
   "Hooks run by proof-shell-insert before inserting a command.
-- 
cgit v1.2.3