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 1d433f848a2f988dd42cde1c313c5048abbc15ad..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