From 69b66557a8bfef7cc4d96fde120d0360f5a94d8b Mon Sep 17 00:00:00 2001
From: Alex Auvolat <alex.auvolat@ens.fr>
Date: Thu, 13 Nov 2014 18:20:40 +0100
Subject: Improve performance by removing useless GUI updates.

---
 judge/main.ml | 19 +++++++++++++------
 1 file changed, 13 insertions(+), 6 deletions(-)

(limited to 'judge/main.ml')

diff --git a/judge/main.ml b/judge/main.ml
index 47d29ba..38de615 100644
--- a/judge/main.ml
+++ b/judge/main.ml
@@ -11,7 +11,7 @@ module UI (C : CORE) : sig
 
   val init : unit -> unit
   val close : unit -> unit
-  val handle_events : unit -> unit
+  val handle_events : unit -> bool
   val display : unit -> unit
 
 end = struct
@@ -41,7 +41,9 @@ end = struct
     | Question of string * (unit -> unit) * view
 
   let rec handle_events () =
+    let usefull = ref false in
     while key_pressed () do
+      usefull := true;
       match !curr_view, read_key() with
       | ScoreBoard, '\t' -> curr_view := MatchList false
       | MatchList _, '\t' -> curr_view := ScoreBoard
@@ -88,7 +90,8 @@ end = struct
             raise Exit_judge),
           v)
       | _ -> ()
-    done
+    done;
+    !usefull
 
   and display () =
     clear_graph ();
@@ -222,12 +225,16 @@ end = struct
   module UI = UI(C)
 
   let run () =
-    C.init();
     UI.init();
+    C.init();
+    let last_r = ref 0.0 in
     begin try while true do
-      C.handle_events ();
-      UI.handle_events ();
-      UI.display ()
+      let a = C.handle_events () in
+      let b = UI.handle_events () in
+      if a || b || Unix.gettimeofday() -. !last_r > 0.1 then begin
+        UI.display ();
+        last_r := Unix.gettimeofday()
+      end
     done with
       Exit_judge ->
         C.finish ();
-- 
cgit v1.2.3