isar-remove-file: remove (tail) recursion, leads to stack overflow

1 files changed, 13 insertions, 11 deletions

diff --git a/isar/isar.el b/isar/isar.el
index 479e4c34..bfabb6d3 100644
--- a/isar/isar.el
+++ b/isar/isar.el
@@ -268,15 +268,17 @@ See -k option for Isabelle interface script."
 ;; Theory loader operations
 ;;
 
-(defun isar-remove-file (name files cmp-base result)
-  (if (not files) (reverse result)
-    (let*
-	((file (car files))
-	 (rest (cdr files))
-	 (same (if cmp-base (string= name (file-name-nondirectory file))
-		 (string= name file))))
-      (if same (isar-remove-file name rest cmp-base result)
-	(isar-remove-file name rest cmp-base (cons file result))))))
+(defun isar-remove-file (name files cmp-base)
+  (let (result)
+    (while files
+      (let*
+	  ((file (car files))
+	   (same (if cmp-base (string= name (file-name-nondirectory file))
+		   (string= name file))))
+	(unless same 
+	  (setq result (cons file result)))
+	(setq files (cdr files))))
+    result))
 
 (defun isar-shell-compute-new-files-list ()
   "Compute the new list of files read by the proof assistant.
@@ -286,9 +288,9 @@ This is called when Proof General spots output matching
       ((name (match-string 1))
        (base-name (file-name-nondirectory name)))
     (if (string= name base-name)
-	(isar-remove-file name proof-included-files-list t nil)
+	(isar-remove-file name proof-included-files-list t)
       (isar-remove-file 
-       (file-truename name) proof-included-files-list nil nil))))
+       (file-truename name) proof-included-files-list nil))))
 
 
 ;;