diff options
Diffstat (limited to 'isar')
-rw-r--r-- | isar/isar.el | 24 |
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)))) ;; |