]> matita.cs.unibo.it Git - helm.git/commitdiff
Bug fixed: the "find" command now scrolls the window appropriately.
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Mon, 18 Jul 2005 16:58:38 +0000 (16:58 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Mon, 18 Jul 2005 16:58:38 +0000 (16:58 +0000)
helm/matita/matitaGui.ml

index 1d433f848a2f988dd42cde1c313c5048abbc15ad..00684d975babda51ef2fd3e0801cc38cc63fe1aa 100644 (file)
@@ -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