From 527599b14b8900f4d32aedd9a6b5d3ec7caa0b8f Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Fri, 2 Oct 1998 13:38:35 +0000
Subject: Added todo for proof-goal-command, proof-save-command

---
 todo | 11 +++++++++++
 1 file changed, 11 insertions(+)

diff --git a/todo b/todo
index d5c4b43e..5e996343 100644
--- a/todo
+++ b/todo
@@ -12,6 +12,17 @@ X (Low)    probably not worth wasting time on
 * This is a list of things which need doing in the generic interface
 ====================================================================
 
+B Improve proof-goal-command and proof-save-command:
+  `proof-goal-command' should be more flexible and support a
+  placeholder for the name and the actual goal. In LEGO, we have
+    Goal foo : absurd;
+    ...
+    Save foo;
+  Perhaps functions at the generic level to make suitable
+  values for the hook, e.g.,
+
+     (setq proof-goal-command  (proof-prompt-named-goal "Goal %s :" "%s;"))
+
 A Change mail address to proofgen@dcs.ed.ac.uk everywhere.
 
 B Cleanup handling of proof-terminal-string.  At the moment some
-- 
cgit v1.2.3