aboutsummaryrefslogtreecommitdiffhomepage
path: root/generic/proof-useropts.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/proof-useropts.el
parent858a775958acb876343155315ecf052d298b797a (diff)
proof-script-command-separator: remove; proof-one-command-per-line becomes prover specific.
Diffstat (limited to 'generic/proof-useropts.el')
-rw-r--r--generic/proof-useropts.el15
1 files changed, 0 insertions, 15 deletions
diff --git a/generic/proof-useropts.el b/generic/proof-useropts.el
index f1019217..6d4fde2a 100644
--- a/generic/proof-useropts.el
+++ b/generic/proof-useropts.el
@@ -215,13 +215,6 @@ files which are out of date with respect to the loaded buffers!"
:type 'boolean
:group 'proof-user-options)
-(defcustom proof-one-command-per-line
- t
- "*If non-nil, format for newlines after each proof command in a script.
-This option is not fully-functional at the moment." ;; TODO
- :type 'boolean
- :group 'proof-user-options)
-
(defcustom proof-prog-name-ask
nil
"*If non-nil, query user which program to run for the inferior process."
@@ -328,14 +321,6 @@ is no locked region."
(const :tag "Automatically process" process))
:group 'proof-user-options)
-(defcustom proof-script-command-separator " "
- "*String separating commands in proof scripts.
-For example, if a proof assistant prefers one command per line, then
-this string should be set to a newline. Otherwise it should be
-set to a space."
- :type 'string
- :group 'proof-user-options)
-
(defcustom proof-rsh-command nil
"*Shell command prefix to run a command on a remote host.
For example,