Re: Widget not destroyed (webkit-gtk bindings)

Adrien <[email protected]> Fri, 23 Jan 2009 11:45:29 +0100
Newsgroups gmane.comp.lang.ocaml.lib.gtk
Message-ID <[email protected]>
Hi,

I finally found the problem. I am now using Gc.full_major as Jacques
Garrigues mentionned in an earlier answer. I had tried using it but
had forgotten a reference to the view.

I also had the following not-so-surprising problem which I failed to
notice : in the following function, Gc.full_major will not finalize
the view.

let kill_view record_with_view_in_it =
  record_with_view_in_it.view#destroy;
  record_with_view_in_it.view <- Obj.magic 0;
  Gc.full_major ()

So I now call Gc.full_major in another function.


 ---

Adrien Nader