max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix(emacs/lean-server): update roi when user changes checking mode

Browse source
This commit is contained in:
Gabriel Ebner 2017-03-24 09:29:06 +01:00
parent 2c7b6fc48f
commit 69f0d30452
1 changed files with 3 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -399,11 +399,11 @@
(and (lean-server-roi-subset-p new-roi old-roi)
(lean-server-roi-subset-p old-roi (lean-server-roi-extend new-roi 10))))
(defun lean-server-sync-roi ()
(defun lean-server-sync-roi (&optional force)
(when lean-server-session
(let ((old-roi (lean-server-session-current-roi lean-server-session))
(new-roi (lean-server-compute-roi lean-server-session)))
(when (or (eq old-roi 'not-yet-sent) (not (lean-server-roi-ok old-roi new-roi)))
(when (or force (eq old-roi 'not-yet-sent) (not (lean-server-roi-ok old-roi new-roi)))
(lean-server-session-send-roi lean-server-session
(lean-server-roi-extend new-roi 5))))))
@ -415,7 +415,7 @@
(defun lean-set-check-mode (mode)
(setq lean-server-check-mode mode)
(lean-server-sync-roi))
(lean-server-sync-roi t))
(defun lean-check-nothing ()
"Check nothing"