Added proof-shell-strip-crs-from-input, and unadvertised proof-script-fly-past-comments

1 files changed, 15 insertions, 1 deletions

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.