Leave blocking section on callback while polling

[btj]

Fixes #141

See also verifast/verifast#252 . With this patch, the VeriFast IDE works correctly and I can no longer get it to crash.

[garrigue]

Interesting. This makes senses, but will have to be tested extensively, on Windows and Linux also.
Note that the function naming may be confusing, but caml_enter_blocking_section actually releases the ocaml global lock, and caml_leave_blocking_section, so this means that we may need to reacquire the lock when calling a callback into ML code.
This is a bit surprising, because I thought that callbacks were only occurring in places where we had already reacquired the lock. This may have been no longer the case with the switch to polling when using GtkThread.

[btj]

Dear @garrigue, your comments make me think that you did not carefully read the linked issue. The problem is that on MacOS, "polling" actually dispatches events.

[garrigue]

OK, now I understand.
The code was assuming that polling was just polling, checking for events without calling callbacks, and MacOS breaks that.
Note that windows is also pretty strange, not allowing you to do GUI operations in another thread, so that you have to queue them using the functions in GtkThread.
Just to be sure, on which architectures did you test your code?
I do not have much time for testing, and I'm afraid to merge this without at least testing on MacOS, Linux and Windows.

[btj]

I (briefly) tested VeriFast built using a lablgtk patched with this PR on Windows, Mac, and Linux. It worked fine. The patch is now in the VeriFast trunk (i.e. in the official nightly builds). Students will be using VeriFast over the course of this month to complete a homework, so additional testing will happen that way.

[garrigue]

Thank you. Testing, particularly on Windows, is always a major difficulty for this kind of problem, so this is very helpful.
I will merge this PR now. Tell me if any problem appears later on.