Configuration changes for shell mode revision.

1 files changed, 8 insertions, 12 deletions

diff --git a/lego/lego.el b/lego/lego.el
index fe73c017..9dc7dd47 100644
--- a/lego/lego.el
+++ b/lego/lego.el
@@ -368,16 +368,12 @@ The directory and extension is stripped of FILENAME before the test."
   (equal module
 	 (file-name-sans-extension (file-name-nondirectory filename))))
 
-(defun lego-shell-compute-new-files-list (str)
-  "Function to update `proof-included-files list'.
+(defun lego-shell-compute-new-files-list ()
+  "Function to update `proof-included-files-list'.
+Value for `proof-shell-compute-new-files-list', which see.
 
-It needs to return an up to date list of all processed files. Its
-output is stored in `proof-included-files-list'. Its input is the
-string of which `lego-shell-retract-files-regexp' matched a
-substring.
-
-We assume that module identifiers coincide with file names."
-  (let ((module (match-string 1 str)))
+For LEGO, we assume that module identifiers coincide with file names."
+  (let ((module (match-string 1)))
     (cdr (member-if
 	  (lambda (filename) (lego-equal-module-filename module filename))
 	  proof-included-files-list))))
@@ -414,9 +410,9 @@ We assume that module identifiers coincide with file names."
 
 	proof-shell-process-file
 	(cons "Creating mark \"\\(.*\\)\" \\[\\(.*\\)\\]"
-	  (lambda (str) (let ((match (match-string 2 str)))
-			  (if (equal match "") match
-			    (concat (file-name-sans-extension match) ".l")))))
+	  (lambda () (let ((match (match-string 2)))
+		       (if (equal match "") match
+			 (concat (file-name-sans-extension match) ".l")))))
 
 	proof-shell-retract-files-regexp
 	"forgot back through Mark \"\\(.*\\)\""