Func menu problems, note added

2 files changed, 6 insertions, 0 deletions

diff --git a/generic/proof-script.el b/generic/proof-script.el
index 93e54789..29a1e268 100644
--- a/generic/proof-script.el
+++ b/generic/proof-script.el
@@ -1456,6 +1456,10 @@ finish setup which depends on specific proof assistant configuration."
     (concat (regexp-quote proof-comment-start) "+\\s_?"))
 
   ;; func-menu --- Jump to a goal within a buffer
+  ;; FIXME 1: is there any way to get this to work for named saves
+  ;; instead of named goals?
+  ;; FIXME 2: each time proof mode is entered these extensions are
+  ;; made!  Probably needs moving out of this function.
   (and (boundp 'fume-function-name-regexp-alist)
        (defvar fume-function-name-regexp-proof
 	 (cons proof-goal-with-hole-regexp 2))
diff --git a/todo b/todo
index 87a2f9b0..25f5c7a7 100644
--- a/todo
+++ b/todo
@@ -36,6 +36,8 @@ C  The semantics of `proof-script-buffer-list' is ambigous. The first
 A Revise ProofGeneral.texi and publish LaTeX version as an LFCS
   Technical Report (2+2 days; da + tms)
 
+A* Bug in proof-mode configuration of func-menu.  (30mins)
+
 A* FIX INDENTATION CODE, EDITING .ML (& other?) FILES IS CHRONICALLY SLOW.
   This is going to hit us hard as soon as the mode gets used in
   earnest.