The callback is inside one thread the call to the gui
and db are protected inside a sync. Especially the fold
left which add each subgoal are each one inside a sync.

Problem you cant select split before all the proof are added.

Perhaps we can
1) add to the model in one thread.
2) acces to the db and the gui inside sync (one sync for each fold_left)