michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

feat(emacs/lean-server): delete cache file (.clean) after visit/load

Browse source 
fix #75
This commit is contained in:
Soonho Kong 2014-10-03 09:44:38 -07:00
parent e255b02fca
commit fffb4e6019
1 changed files with 17 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

19
src/emacs/lean-server.el
View file

@ -242,11 +242,26 @@ If it's not the same with file-name (default: buffer-file-name), send VISIT cmd.
('WAIT (lean-server-check-current-file))
('SYNC )))
(defun lean-server-delete-cache-file ()
"Delete the .clean file for the current buffer (if any)"
(let* ((file-name (buffer-file-name))
(ext (and file-name (f-ext file-name)))
cache-file-name
)
(when (string= ext "lean")
(setq cache-file-name
(concat (f-no-ext file-name)
".clean"))
(when (f-file? cache-file-name)
(lean-debug "Delete cache file %s" cache-file-name)
(ignore-errors
(delete-file cache-file-name))))))
(defun lean-server-after-send-cmd (cmd)
"Operations to perform after sending a command."
(cl-case (lean-cmd-type cmd)
('LOAD ())
('VISIT ())
('LOAD (lean-server-delete-cache-file))
('VISIT (lean-server-delete-cache-file))
('REPLACE ())
('INSERT ())
('REMOVE ())