]> matita.cs.unibo.it Git - helm.git/commit
Code changed a bit to make it work as before with OCaml 4.0.
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Fri, 7 Mar 2014 18:05:12 +0000 (18:05 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Fri, 7 Mar 2014 18:05:12 +0000 (18:05 +0000)
commit84cc672d70212e4f204bc2f43120ec4d82f9bcd9
tree726ed776ec35830097c92afcb123213cb2df0f07
parent5072e94b40c0a9b9ed010d49c244d00ee30a7395
Code changed a bit to make it work as before with OCaml 4.0.
Without this patch, the refresh of the textual widget (e.g. the update
of the locked part) is not immediately done.

This is roughly the visual behaviour the user expects. On the other hand,
we also expect the threads that execute and that responsible for the UI
to work in parallel, which is not the case. The code I just touched stops
the worker thread for, on average, 0.1s per tactic, which is really a lot.
Switching to a multiprocess implementation (in place of a multithread) does
not seem easy. Bad OCaml, bad.
matita/matita/matitaScript.ml