From 230e6cf0fa993e20a46a44aa5fcbc8ad9484e677 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Sun, 19 Oct 2008 08:21:48 +0000 Subject: [PATCH] when a file is opened the cursor is moved to the begin of the file --- helm/software/matita/matitaGui.ml | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/helm/software/matita/matitaGui.ml b/helm/software/matita/matitaGui.ml index c65104035..1fe78046e 100644 --- a/helm/software/matita/matitaGui.ml +++ b/helm/software/matita/matitaGui.ml @@ -843,6 +843,8 @@ class gui () = source_view#source_buffer#begin_not_undoable_action (); script#loadFromFile f; source_view#source_buffer#end_not_undoable_action (); + source_view#buffer#move_mark `INSERT source_view#buffer#start_iter; + source_view#buffer#place_cursor source_view#buffer#start_iter; console#message ("'"^f^"' loaded.\n"); self#_enableSaveTo f | None -> () @@ -1134,6 +1136,8 @@ class gui () = source_view#source_buffer#begin_not_undoable_action (); script#loadFromFile content; source_view#source_buffer#end_not_undoable_action (); + source_view#buffer#move_mark `INSERT source_view#buffer#start_iter; + source_view#buffer#place_cursor source_view#buffer#start_iter; console#message ("'"^file^"' loaded."); self#_enableSaveTo file -- 2.39.2