On Wednesday 16 July 2008 17:44:18 Claudio Sacerdoti Coen wrote:
> Dear Yang,
>
> not every node is an element. Thus you need to use dinamic cast:
>
> let node = ... in
>   (* next line may raise GdomeInit.DOMCastException *)
> let element = Gdome.element_of_node node in
>   ...

Thank you very much. I haven't noticed element_of_node. As 
Gdome.element_of_node is a class and there is no equivalent function, thus my 
final version is like is:

let element = new Gdnome.element_of_node node in

> 						Cheers,
> 						C.S.C.
> On Wed, 2008-07-16 at 17:13 +0800, Yang Shouxun wrote:
> > Hello everyone,
> >
> > I've been using Gdome for some time now and I always find it difficult to
> > deal with the type system. Here is the issue:
> >
> > The document class has a
> >  method getElementsByTagName :
> >       tagname:Gdome.domString -> Gdome.nodeList
> > and from a nodeList object I can only get Gdome.node objects, while we
> > know they should be Gdome.element objects.
> >
> > My question is how to convert from Gdome.node to Gdome.element?
> >
> > P.S. Gdome.element can be converted to Gdome.node, but not in the other
> > direction as far as I know.
> >
> > TIA,
> >
> > shouxun