diff options
Diffstat (limited to 'otherlibs')
| -rw-r--r-- | otherlibs/graph/graphics.ml | 12 | ||||
| -rw-r--r-- | otherlibs/graph/graphics.mli | 8 |
2 files changed, 20 insertions, 0 deletions
diff --git a/otherlibs/graph/graphics.ml b/otherlibs/graph/graphics.ml index c45c5bfcab..441c6760cd 100644 --- a/otherlibs/graph/graphics.ml +++ b/otherlibs/graph/graphics.ml @@ -212,6 +212,18 @@ let read_key () = let key_pressed () = let e = wait_next_event [Poll] in e.keypressed +let loop_at_exit events handler = + let events = List.filter (fun e -> e <> Poll) events in + at_exit (fun _ -> + try + while true do + let e = wait_next_event events in + handler e + done + with Exit -> close_graph () + | e -> close_graph (); raise e + ) + (*** Sound *) external sound : int -> int -> unit = "caml_gr_sound" diff --git a/otherlibs/graph/graphics.mli b/otherlibs/graph/graphics.mli index e1dce5263c..81cd4eeb05 100644 --- a/otherlibs/graph/graphics.mli +++ b/otherlibs/graph/graphics.mli @@ -303,6 +303,14 @@ external wait_next_event : event list -> status = "caml_gr_wait_event" are queued, and dequeued one by one when the [Key_pressed] event is specified. *) +val loop_at_exit : event list -> (status -> unit) -> unit +(** Loop before exiting the program, the list given as argument is the + list of handlers and the events on which these handlers are called. + To exit cleanly the loop, the handler should raise Exit. Any other + exception will be propagated outside of the loop. + @since 4.01 +*) + (** {6 Mouse and keyboard polling} *) val mouse_pos : unit -> int * int |