m-fleury / isabelle-emacs

Clone of isabelle, with LSP extensions in seperate branches
Other
25 stars 5 forks source link

Erratic cursor behaviour #31

Closed m-fleury closed 4 years ago

m-fleury commented 4 years ago

Sometimes the cursor jumps around.

m-fleury commented 4 years ago

After managing to more or less consistently reproduce it yesterday, I think that I have now fixed it in commit a43ad6645d243b6465f3d6be0b874c46e0fa16e0.

Long explanation

Goal printing asynchronously uses the following function:

   (async-start
         < do something in a separate emacs>
         (lambda (result)
            (save-excursion
                <do something with the result>)))

What can wrong here?

The execution of other runners can be interrupted by signals. The scenario where the bug happened is the following:

  1. emacs receives a goal to print;
  2. it starts the asynchronous process;
  3. it receives decorations to print;
  4. the position of the cursor is saved by save-excursion and decorations are printed;
  5. the asynchronous return the result;
  6. the decoration printing is interrupted;
  7. the position of the cursor is lost;
  8. the result from the asynchronous process is processed;
  9. the remaining decorations are printed.

The interesting side effect of the scenario is that the debugger is not helpful to find those bugs.

The solution was to change the asynchronous position to:

   (save-excursion
     (async-start
           < do something in a separate emacs>
           (lambda (result)
                <do something with the result>)))

Why did not you do that before?

Well, because the asynchronous part has no effect on the current buffer and that I don't want to restore the position of the cursor when the beginning of the function call, but only the cursor after asynchronous processing.

So your fix makes no sense right? Now the cursor from the beginning of the process is restored?

This is the part where I don't have a proper answer. I believe that the difference lies in the recursive-edit merger from emacs: it now understands the intended meaning (don't move the cursor) and acts like the execution took no time.

However, documentation on that part of emacs is very scarce and it is a bug that is very hard to reproduce.

What are the drawbacks?

It feels like emacs is now a tiny bit slower, but it could be only a feeling or something else that changed during the refactoring.

Things I don't really understand yet

m-fleury commented 4 years ago

That could potentially be also the reason of #29 (depending on how things are merged).