Code simplification.

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

diff --git a/helm/matita/matitaGui.ml b/helm/matita/matitaGui.ml
index 216dc9d5b79d2cbef8536142a6332ffce2f20db8..066d07cc5af2c0e387748052fbdc3e65bf2e45c4 100644 (file)
--- a/helm/matita/matitaGui.ml
+++ b/helm/matita/matitaGui.ml
@@ -355,9 +355,8 @@ class gui () =
         ~callback:(fun () -> ignore (source_view#buffer#delete_selection ())));
       ignore(self#main#selectAllMenuItem#connect#activate
         ~callback:(fun () ->
-          source_buffer#move_mark `INSERT (source_buffer#get_iter `START);
-          source_buffer#move_mark `SEL_BOUND (source_buffer#get_iter `END)
-          ));
+          source_buffer#move_mark `INSERT source_buffer#start_iter;
+          source_buffer#move_mark `SEL_BOUND source_buffer#end_iter));
       ignore(self#main#findReplMenuItem#connect#activate
         ~callback:show_find_Repl);
       ignore (findRepl#findEntry#connect#activate ~callback:find_forward);