Bug fixed: the "find" command now scrolls the window appropriately.

[helm.git] / helm / matita / matitaGui.ml

diff --git a/helm/matita/matitaGui.ml b/helm/matita/matitaGui.ml
index efe629ac1903d8954781314b1109bdefbf34d8f2..00684d975babda51ef2fd3e0801cc38cc63fe1aa 100644 (file)
--- a/helm/matita/matitaGui.ml
+++ b/helm/matita/matitaGui.ml
@@ -170,7 +170,8 @@ class gui () =
       let find_forward _ = 
           let highlight start end_ =
             source_buffer#move_mark `INSERT ~where:start;
-            source_buffer#move_mark `SEL_BOUND ~where:end_
+            source_buffer#move_mark `SEL_BOUND ~where:end_;
+            source_view#scroll_mark_onscreen `INSERT
           in
           let text = findRepl#findEntry#text in
           let iter = source_buffer#get_iter `SEL_BOUND in
@@ -225,16 +226,21 @@ class gui () =
           | None -> ()
           | Some d -> MatitamakeLib.destroy_development d);
           refresh_devels_win ());
+      let refresh () = 
+        while Glib.Main.pending () do 
+          ignore(Glib.Main.iteration false); 
+        done
+      in
       connect_button develList#buildButton 
         (fun () -> 
           match get_devel_selected () with
           | None -> ()
-          | Some d -> ignore(MatitamakeLib.build_development d));
+          | Some d -> ignore(MatitamakeLib.build_development_in_bg refresh d));
       connect_button develList#cleanButton 
         (fun () -> 
           match get_devel_selected () with
           | None -> ()
-          | Some d -> ignore(MatitamakeLib.clean_development d));
+          | Some d -> ignore(MatitamakeLib.clean_development_in_bg refresh d));
       connect_button develList#closeButton 
         (fun () -> develList#toplevel#misc#hide());
       ignore(develList#toplevel#event#connect#delete