From 29f6b9e091e896d98505a0aa62dcac13f8896343 Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Wed, 29 Sep 1999 15:44:53 +0000
Subject: Added proof-script-command-separator.  Needs work.

---
 generic/proof-config.el | 10 ++++++++++
 todo                    |  3 +++
 2 files changed, 13 insertions(+)

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,
diff --git a/todo b/todo
index b4625739..f0e2e8e8 100644
--- a/todo
+++ b/todo
@@ -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.
-- 
cgit v1.2.3