use-old-parser setting replaces use-new-parser setting [WARNING: big change]

1 files changed, 9 insertions, 0 deletions

diff --git a/generic/proof-config.el b/generic/proof-config.el
index c8dac4ac..4bf9f269 100644
--- a/generic/proof-config.el
+++ b/generic/proof-config.el
@@ -843,6 +843,15 @@ or `proof-script-parse-function'."
   :type 'string
   :group 'prover-config)
 
+(defcustom proof-script-use-old-parser nil
+  "Whether to use the old parsing mechanism.
+This is a stop-gap option in Proof General 3.4 added for
+proof assistants which still depend on peculiarities of the old
+parsing functions. (Specific example: Isar relies on certain
+text being sent to prover which according to syntax configuration
+are comments; new parser does not send these currently.)"
+  :type 'boolean
+  :group 'prover-config)
 
 (defcustom proof-script-integral-proofs nil
   "Whether the complete text after a goal confines the actual proof.