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 51b17451e9caa1c1bbd9d964930dcd46368dd61b..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 
@@ -322,19 +328,20 @@ class gui () =
                 (fun _ -> adj#set_value (adj#upper -. adj#page_size)));
       console#message (sprintf "\tMatita version %s\n" BuildTimeConf.version);
         (* toolbar *)
-      let module A = TacticAst in
-      let hole = CicAst.UserInput in
-      let loc = CicAst.dummy_floc in
+      let module A = GrafiteAst in
+      let hole = CicNotationPt.UserInput in
+      let loc = Disambiguate.dummy_floc in
       let tac ast _ =
         if (MatitaScript.instance ())#onGoingProof () then
           (MatitaScript.instance ())#advance
-            ~statement:("\n" ^ TacticAstPp.pp_tactical (A.Tactic (loc, ast))) ()
+            ~statement:("\n" ^ GrafiteAstPp.pp_tactical (A.Tactic (loc, ast)))
+            ()
       in
       let tac_w_term ast _ =
         if (MatitaScript.instance ())#onGoingProof () then
           let buf = source_buffer in
           buf#insert ~iter:(buf#get_iter_at_mark (`NAME "locked"))
-            ("\n" ^ TacticAstPp.pp_tactic ast)
+            ("\n" ^ GrafiteAstPp.pp_tactic ast)
       in
       let tbar = self#main in
       connect_button tbar#introsButton (tac (A.Intros (loc, None, [])));