Date: Wed, 10 Aug 2005 15:42:41 +0900 (JST)
Message-Id: <20050810.154241.86370584.garrigue at math.nagoya-u.ac.jp>
To: shoh at compiler.kaist.ac.kr
Cc: lablgtk at math.nagoya-u.ac.jp
Subject: Re: Two question about selection
From: Jacques Garrigue <garrigue at math.nagoya-u.ac.jp>
In-Reply-To: <42F98026.8070602 at compiler.kaist.ac.kr>
References: <42F96DA8.7050003 at compiler.kaist.ac.kr>
	<20050810.125349.79297434.garrigue@math.nagoya-u.ac.jp>
	<42F98026.8070602@compiler.kaist.ac.kr>
Mime-Version: 1.0
Content-Type: Text/Plain; charset=us-ascii
Content-Transfer-Encoding: 7bit

From: SooHyoung Oh <shoh at compiler.kaist.ac.kr>

> Can you give me more hints about how to convert string to *** atom list ***?

I had not realized that this example actually used a string as an
array of atoms...
So of course, you would need some amount of magic to extract the
corresponding values.
Fortunately, atoms are simply encoded as integers, 
so you should be able to work this way:

let wsize = Sys.word_size / 8
let atoms_of_string s =
  let len = String.length s / wsize in
  let arr = Array.create len Gdk.Atom.none in
  for i = 0 to len - 1 do
    let a = String.sub s (i*wsize) wsize in
    let b : Gpointer.boxed = Obj.magic (0, a) in
    let n = Nativeint.to_int (Gpointer.peek_nativeint b) in
    arr.(i) <- Obj.magic n
  done;
  arr

This may seem a bit complicated, but I don't see any simpler way.

Jacques