aboutsummaryrefslogtreecommitdiffhomepage
path: root/generic/pg-custom.el
diff options
context:
space:
mode:
authorGravatar David Aspinall <da@inf.ed.ac.uk>2010-10-01 14:36:12 +0000
committerGravatar David Aspinall <da@inf.ed.ac.uk>2010-10-01 14:36:12 +0000
commitb2b6d6b9824c921a1f3a920871817fefcd6eccfc (patch)
treedf35addf8a5279431296ee38a687653a37742fa1 /generic/pg-custom.el
parent858a775958acb876343155315ecf052d298b797a (diff)
proof-script-command-separator: remove; proof-one-command-per-line becomes prover specific.
Diffstat (limited to 'generic/pg-custom.el')
-rw-r--r--generic/pg-custom.el11
1 files changed, 10 insertions, 1 deletions
diff --git a/generic/pg-custom.el b/generic/pg-custom.el
index fd5c1a23..d85a1819 100644
--- a/generic/pg-custom.el
+++ b/generic/pg-custom.el
@@ -30,7 +30,8 @@
;;; Code:
-(require 'proof-utils) ; defpgcustom
+(require 'pg-pamacs) ; defpgcustom
+(require 'pg-vars) ; for proof-next-command-on-new-line
(require 'proof-config) ; for proof-toolbar-entries-default
(defpgcustom script-indent t
@@ -158,6 +159,14 @@ Currently this setting is UNIMPLEMENTED, changes have no effect."
:type 'boolean
:group 'prover-config)
+(defpgcustom one-command-per-line
+ (cond
+ ((eq proof-assistant-symbol 'isar) nil)
+ (t t))
+ "*If non-nil, format for newlines after each command in a script."
+ :type 'boolean
+ :group 'proof-user-options)
+
;; Contributed modes