Add proof-electric-terminator-noterminator behaviour for Isar

2 files changed, 11 insertions, 8 deletions

diff --git a/generic/pg-user.el b/generic/pg-user.el
index 2a8590f8..d226aa49 100644
--- a/generic/pg-user.el
+++ b/generic/pg-user.el
@@ -492,7 +492,7 @@ This is intended as a value for `proof-activate-scripting-hook'"
   ;;          (2) needs this name to be recognized in
   ;;		  proof-assert-until-point
   (setq incomment t)
-  (if ins (backward-delete-char 1))
+  (if ins (backward-delete-char 1)) ; delete spurious char in comment
   (goto-char mrk)
   (insert proof-terminal-string))
 
@@ -518,17 +518,15 @@ comment, and insert or skip to the next semi)."
 	;; In locked region, just insert terminator without further ado
 	(insert proof-terminal-char)
       ;; Otherwise, do other thing.
-      ;; Old idea: only shift terminator wildly if we're looking at
-      ;; whitespace.  Why?
-      ;; (if (looking-at "\\s-\\|\\'\\|\\w")
       (if (proof-only-whitespace-to-locked-region-p)
 	  (error "There's nothing to do!"))
 
       (if (not (= (char-after (point)) proof-terminal-char))
 	  (progn
 	    (forward-char) ;; immediately after command end.
-	    (insert proof-terminal-string)
-	    (setq ins t)))
+	    (unless proof-electric-terminator-noterminator
+	      (insert proof-terminal-string)
+	      (setq ins t))))
       (proof-assert-until-point 'proof-electric-term-incomment-fn)
       (or incomment
 	  (proof-script-next-command-advance)))))
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)