renamed fume-match-find-next-function-name

2 files changed, 31 insertions, 50 deletions

diff --git a/generic/proof.el b/generic/proof.el
index 7fe152e5..91036383 100644
--- a/generic/proof.el
+++ b/generic/proof.el
@@ -687,6 +687,24 @@ is resynchronised. It contains files in canonical truename format")
 ;; A few small utilities					    ;;
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 
+(defun proof-match-find-next-function-name (buffer)
+  "General next function name in BUFFER finder using match.
+The regexp is assumed to be a two item list the car of which is the regexp
+to use, and the cdr of which is the match position of the function
+name. Moves point after the match.
+
+The package fume-func provides the function
+`fume-match-find-next-function-name' with the same specification.
+However, fume-func's version is incorrec"
+  ;; DO NOT USE save-excursion; we need to move point!
+  ;; save-excursion is called at a higher level in the func-menu
+  ;; package 
+    (set-buffer buffer)
+    (let ((r (car fume-function-name-regexp))
+	  (p (cdr fume-function-name-regexp)))
+      (and (re-search-forward r nil t)
+	   (cons (buffer-substring (setq p (match-beginning p)) (point)) p))))
+
 (defun proof-message (str)
   "Output STR in minibuffer."
   (message (concat "[" proof-assistant "] " str)))
@@ -951,25 +969,6 @@ buffer is closed off atomically."
                               nil (or history
                               'shell-command-history)))))
 
-;; The package fume-func provides a function with the same name and
-;; specification. However, fume-func's version is incorrect.
-;; da: make this hack more prominent so someone remembers to remove it
-;; later on.
-(and (fboundp 'fume-match-find-next-function-name)
-(defun fume-match-find-next-function-name (buffer)
-  "General next function name in BUFFER finder using match.
-The regexp is assumed to be a two item list the car of which is the regexp
-to use, and the cdr of which is the match position of the function
-name. Moves point after the match."
-  ;; DO NOT USE save-excursion; we need to move point!
-  ;; save-excursion is called at a higher level in the func-menu
-  ;; package 
-    (set-buffer buffer)
-    (let ((r (car fume-function-name-regexp))
-	  (p (cdr fume-function-name-regexp)))
-      (and (re-search-forward r nil t)
-	   (cons (buffer-substring (setq p (match-beginning p)) (point)) p)))))
-
 
 ;;; end messy COMPATIBILITY HACKING
 
@@ -2864,7 +2863,7 @@ finish setup which depends on specific proof assistant configuration."
        (push (cons major-mode 'fume-function-name-regexp-proof)
 	     fume-function-name-regexp-alist))
   (and (boundp 'fume-find-function-name-method-alist)
-       (push (cons major-mode 'fume-match-find-next-function-name)
+       (push (cons major-mode 'proof-match-find-next-function-name)
 	     fume-find-function-name-method-alist))
 
   ;; Additional key definitions which depend on configuration for
diff --git a/todo b/todo
index 18899a30..bedf88dc 100644
--- a/todo
+++ b/todo
@@ -54,17 +54,17 @@ C Remove .gif, .jpg, .xpm, .xbm files from the CVS repository.  Add
   to have the Gimp installed to build them via 'make images'
   (or copy them from the latest download).   (da, 1hr)
 
-B proof-issue-goal should refuse to work when a proof is in progress.
+C proof-issue-goal should refuse to work when a proof is in progress.
   Similarly proof-issue-save should refuse to work when a proof
   hasn't been completed! Algorithm: Search the last goal and check
   length of span.  (45min)
 
-B Bug in proof-retract-until-point when called twice in succession:
+C Bug in proof-retract-until-point when called twice in succession:
   calls backward-char at beginning of buffer.  (Should say no
   locked region, or "nothing to retract").  Problems is that
   there is a proof-locked-end, but it's at (point-min). (30min)
 
-B proof-find-next-terminator doesn't work properly:
+C proof-find-next-terminator doesn't work properly:
 
      first;second;third
            ^
@@ -76,7 +76,7 @@ B proof-find-next-terminator doesn't work properly:
 B Add proof-rsh-command and note in documentation about how to
   use widely-advertised "remote shell" feature.  (1hr)
 
-D Add proof-quit-command: some provers may like a quit command to be
+B Add proof-quit-command: some provers may like a quit command to be
   sent to the shell, not just EOF !  (see proof-stop-shell).
   Also reconcile proof-restart-script and proof-stop-shell, see
   comments in code.
@@ -84,7 +84,7 @@ D Add proof-quit-command: some provers may like a quit command to be
 D Multiple files: handle failures in
   reading ancestors.
 
-B Clean up proof-assert-until-point behaviour.  Discussion results:
+C Clean up proof-assert-until-point behaviour.  Discussion results:
     1.  At the moment we get an odd error if it is run in
     the locked region.    This is a bug.  Should behave same
     as proof-assert-next-command in this case (simpler) or
@@ -98,15 +98,11 @@ B Clean up proof-assert-until-point behaviour.  Discussion results:
      proof-assert-next-command for now, eventually 
      this may form a new version of proof-assert-until-point]
 
-    3.  Toolbar movement functions should operate just on the locked
-    region, and not move point.  They should maintain visibility of
-    end of locked region, though.
-
-    4.  Movement and possible insertion of spaces/newlines for 
+    3.  Movement and possible insertion of spaces/newlines for 
     when new commands are added to the buffer needs careful
     thought! (1h)
 
-A Implement more generic mechanism for large undos (2h tms)
+B Implement more generic mechanism for large undos (2h tms)
 
     COQ: C-c u inside a Section should reset the whole section, then
          redo defns 
@@ -117,7 +113,7 @@ A Implement more generic mechanism for large undos (2h tms)
 A replace (current-buffer) by proof-shell-buffer/proof-script-buffer
   where ever possible (30 min tms)
 
-B New buffer model (4h):
+A New buffer model (4h):
 
     1. Script buffers
     2. Response buffer
@@ -125,7 +121,7 @@ B New buffer model (4h):
     4. (hidden) process buffer
     5. Minibuffer for additionally sending information to the process 
 
-B Revise ProofGeneral.texi and publish LaTeX version as an LFCS
+A Revise ProofGeneral.texi and publish LaTeX version as an LFCS
   Technical Report (2 days; da + tms)
 
 C Provide a sensible default frame/buffer layout (4h)
@@ -167,11 +163,6 @@ C Investigate and improve indentation/font-locking code.
   *very* slow.  Moreover the indentation is screwy.  Also
   seems screwy in LEGO/Coq PG.  (da, 2hr)
 
-C Improve Linux install via spec file: hack the load line into 
-  site-start.el.  Could use emacs to determine its location,
-  automatically detect both XEmacs and Emacs, etc.  See if
-  other Emacs packages do something clever. 
-
 B Split code; particularly proof.el Warning: we need to synchronise
    code before!(1h)
 
@@ -201,7 +192,7 @@ C User-level functions:
 C Write test schedule for things to try out with a new instantiation
   of Proof General.
 
-B Add skeleton instantiation files for a dummy prover "myassistant" to
+C Add skeleton instantiation files for a dummy prover "myassistant" to
   make it easier to add support for new assistants -- looking at
   any of the existing modes is confusing because of the
   prover-specific stuff.  Ideally it should work for one of
@@ -212,8 +203,6 @@ D Code in proof.el assumes all characters with top bit set are special
   instructions to Emacs.  This is rather arrogant, and precludes proof
   systems which utilize 8-bit character sets!  Needs repair.  (3h)
 
-D Prune dead code.  (1h)
-
 D Add support to proof.el for *not* setting variables for
   commands which aren't supported by a prover.  For example,
   in Isabelle there is no such thing as killing a goal.
@@ -223,10 +212,6 @@ D Add support to proof.el for *not* setting variables for
 D Outsource script management features from proof.el to
   proof-script.el 		(1h)
 
-D Improve documentation in proof.el to help porting/understanding 
-  Also add notes into proof.texinfo.
-  (ongoing, da).
-
 C Fixup sources to follow Elisp conventions better.
   1. The first line of documentation of functions and
      variables should be a whole sentence.  Subsequent lines should
@@ -242,13 +227,13 @@ C Fixup sources to follow Elisp conventions better.
 D Implement proof-find-previous-terminator and bind it to C-c C-a
   (45min)
 
-B file handling could be more robust; perhaps one should always cd to
+C file handling could be more robust; perhaps one should always cd to
   the directory corresponding to the script buffer (currently only
   done for the buffer which starts up the proof system). This could be 
   achieved with a hook which is not set by default. [Remember to add
   user documentation] (30min tms)
 
-B Reengineer *-count-undos and *-find-and-forget at generic level
+C Reengineer *-count-undos and *-find-and-forget at generic level
   (3h)
 
 D Allow bib-cite style clicking on Load/Import commands to go to file.
@@ -260,9 +245,6 @@ C Unify toolbar and menu functions.
 D Remove duplication of variables e.g., proof-prog-name and
   lego-prog-name for Coq and Lego. (1h)
 
-D Fixup implementation of "spans":  Add documentation!
-  (30 mins)
-
 C Make completion more generic. For Isabelle and Lego, we can build a
   completion table by querying the process, which is better than
   messing with tags.