diff options
| -rw-r--r-- | generic/proof-config.el | 10 | ||||
| -rw-r--r-- | todo | 3 |
2 files changed, 13 insertions, 0 deletions
diff --git a/generic/proof-config.el b/generic/proof-config.el index aa6294ed..2da756cf 100644 --- a/generic/proof-config.el +++ b/generic/proof-config.el @@ -150,12 +150,22 @@ provers. Enable it if it works for you." :type 'boolean :group 'proof-general) +;; FIXME: rationalize and combine next two (defcustom proof-one-command-per-line nil "*If non-nil, format for newlines after each proof command in a script. This option is not fully-functional at the moment." :type 'boolean :group 'proof-general) + +(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-general) + (defcustom proof-rsh-command "" "*Shell command prefix to run a command on a remote host. For example, @@ -57,6 +57,9 @@ A Usability enhancement: - Fix asymmetry between "doing" and "undoing": doing will skip comments, undoing will not. e.g. test case: (* tester *) intros; +A Usability enhancement: + - Fix proof-script-command-separator and proof-one-command-per-line flag. + C Compatibility enhancement: - Consider sending comments to proof process after all. They might contain special (e.g. LaTeX) directives or something. |