From d5a0b9024ec59523d0744efdceda30adff2a7969 Mon Sep 17 00:00:00 2001 From: David Aspinall Date: Tue, 26 May 2009 09:33:36 +0000 Subject: Add proof-electric-terminator-noterminator behaviour for Isar --- generic/proof-config.el | 9 +++++++-- 1 file changed, 7 insertions(+), 2 deletions(-) (limited to 'generic/proof-config.el') 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 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) -- cgit v1.2.3