aboutsummaryrefslogtreecommitdiffhomepage
path: root/generic/proof-useropts.el
diff options
context:
space:
mode:
Diffstat (limited to 'generic/proof-useropts.el')
-rw-r--r--generic/proof-useropts.el8
1 files changed, 8 insertions, 0 deletions
diff --git a/generic/proof-useropts.el b/generic/proof-useropts.el
index d228016c..0a7d8bfe 100644
--- a/generic/proof-useropts.el
+++ b/generic/proof-useropts.el
@@ -71,6 +71,14 @@ terminator somewhere nearby. Electric!"
:set 'proof-set-value
:group 'proof-user-options)
+(defcustom proof-next-command-insert-space t
+ "*If non-nil, PG will use heuristics to insert newlines or spaces in scripts.
+In particular, if electric terminator is switched on, spaces or newlines will
+be inserted as the user types commands to the prover."
+ :type 'boolean
+ :set 'proof-set-value
+ :group 'proof-user-options)
+
(defcustom proof-toolbar-enable t
"*If non-nil, display Proof General toolbar for script buffers."
:type 'boolean