Re: Unix.sleep et bibliothèque graphique

[Xavier Leroy <Xavier.Leroy@inria.fr>]

[English summary: Laure observed that Unix.sleep returns early when
the graphics window is open.  Under Unix, the graphics library uses
signals for event processing, and on many Unix systems, Unix.sleep
returns early when interrupted by a signal.  Here is an alternate
implementation of sleep that is robust against signals.]

> suite à quelques essais infructeux et de discussions, voici un
> résumé du pb : il s'agit de mettre des pauses au milieu de
> programmes graphiques qui s'éxécutent trop vite
> 1) Le programme suivant [avec Unix.sleep] marche bien.
> 2) Par contre, si j'ajoute open_graph "", cela               
> ne marche plus.                                              

Oui, sur certains systèmes Unix, la fonction Unix.sleep retourne dès
que le processus reçoit un signal, sans attendre la fin du délai
prescrit.  Or, il se trouve que la bibliothèque Graphics utilise des
signaux (pour traiter les événements X de manière asynchrone).

Ce problème n'est pas facile à contourner, il a fallu que je me gratte
la tête un moment, mais voici une réimplémentation de Unix.sleep qui
ne présente pas cet inconvénient:

let mysleep n =
  let start = Unix.gettimeofday() in
  let rec delay t =
    try
      ignore (Unix.select [] [] [] t)
    with Unix.Unix_error(Unix.EINTR, _, _) ->
      let now = Unix.gettimeofday() in
      let remaining = start +. n -. now in
      if remaining > 0.0 then delay remaining in
  delay n

Attention, le paramètre de délai est un flottant, non un entier, ce
qui permet aussi de suspendre le programme pour moins d'une seconde.

Essayez, cela devrait marcher dans un programme utilisant Graphics.

- Xavier Leroy