aboutsummaryrefslogtreecommitdiffhomepage
path: root/generic/proof-config.el
diff options
context:
space:
mode:
authorGravatar David Aspinall <da@inf.ed.ac.uk>2009-05-26 09:33:36 +0000
committerGravatar David Aspinall <da@inf.ed.ac.uk>2009-05-26 09:33:36 +0000
commitd5a0b9024ec59523d0744efdceda30adff2a7969 (patch)
tree63baa0118abb6441be3c160eaadd8f355a02a093 /generic/proof-config.el
parentb2ab0c0ccc9637b6c467e65183653b4366854919 (diff)
Add proof-electric-terminator-noterminator behaviour for Isar
Diffstat (limited to 'generic/proof-config.el')
-rw-r--r--generic/proof-config.el9
1 files changed, 7 insertions, 2 deletions
diff --git a/generic/proof-config.el b/generic/proof-config.el
index b83ca8e8..c3f13b4b 100644
--- a/generic/proof-config.el
+++ b/generic/proof-config.el
@@ -1,6 +1,6 @@
;;; proof-config.el --- Proof General configuration for proof assistant
;;
-;; Copyright (C) 1998-2008 LFCS Edinburgh.
+;; Copyright (C) 1998-2009 LFCS Edinburgh.
;; Author: David Aspinall <David.Aspinall@ed.ac.uk> and others
;; License: GPL (GNU GENERAL PUBLIC LICENSE)
;;
@@ -773,6 +773,11 @@ or `proof-script-parse-function'."
:type 'character
:group 'prover-config)
+(defcustom proof-electric-terminator-noterminator nil
+ "If non-nil, electric terminator does not actually insert a terminator."
+ :type 'boolean
+ :group 'prover-config)
+
(defcustom proof-script-sexp-commands nil
"Non-nil if script has LISP-like syntax: commands are top-level sexps.
You should set this variable in script mode configuration.
@@ -1836,7 +1841,7 @@ The default value is \"\\n\" to match up to the end of the line."
At the moment, this setting is not used in the generic Proof General.
-Future use may providea generic implementation for `pg-topterm-goalhyplit-fn',
+Future use may provide a generic implementation for `pg-topterm-goalhyplit-fn',
used to help parse the goals buffer to annotate it for proof by pointing."
:type '(choice regexp (const :tag "Unset" nil))
:group 'proof-shell)