Highlighting of parse errors implemented.

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

diff --git a/helm/matita/matitaGui.ml b/helm/matita/matitaGui.ml
index f83e01913d7fb1c26281e4ef5a60492e39301b67..733d0aab9699e37a5fd59fb9168a96dc674a10af 100644 (file)
--- a/helm/matita/matitaGui.ml
+++ b/helm/matita/matitaGui.ml
@@ -331,6 +331,18 @@ class gui () =
       let clipboard =
        let atom = Gdk.Atom.clipboard in
         GData.clipboard atom in
+      ignore(self#main#editMenu#connect#activate
+        ~callback:
+          (fun () ->
+            let something_selected =
+              (source_buffer#get_iter_at_mark `INSERT)#compare
+              (source_buffer#get_iter_at_mark `SEL_BOUND) <> 0
+            in
+             self#main#cutMenuItem#misc#set_sensitive something_selected;
+             self#main#copyMenuItem#misc#set_sensitive something_selected;
+             self#main#deleteMenuItem#misc#set_sensitive something_selected;
+             self#main#pasteMenuItem#misc#set_sensitive (clipboard#text <> None)
+          ));
       ignore(self#main#cutMenuItem#connect#activate
         ~callback:(fun () -> source_view#buffer#cut_clipboard clipboard));
       ignore(self#main#copyMenuItem#connect#activate
@@ -341,6 +353,10 @@ class gui () =
           (MatitaScript.instance ())#clean_dirty_lock));
       ignore(self#main#deleteMenuItem#connect#activate
         ~callback:(fun () -> ignore (source_view#buffer#delete_selection ())));
+      ignore(self#main#selectAllMenuItem#connect#activate
+        ~callback:(fun () ->
+          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);
@@ -358,8 +374,13 @@ class gui () =
       let locker f = 
         fun () -> 
           lock_world ();
-          try f ();unlock_world () with exc -> unlock_world (); raise exc
-      in
+          try f ();unlock_world () with exc -> unlock_world (); raise exc in
+      let keep_focus f =
+        fun () ->
+         try
+          f (); source_view#misc#grab_focus ()
+         with
+          exc -> source_view#misc#grab_focus (); raise exc in
         (* developments win *)
       let model = 
         new MatitaGtkMisc.multiStringListModel 
@@ -615,19 +636,17 @@ class gui () =
       in
       let cursor () =
         source_buffer#place_cursor
-          (source_buffer#get_iter_at_mark (`NAME "locked"));
-        source_view#misc#grab_focus ()
-      in
+          (source_buffer#get_iter_at_mark (`NAME "locked")) in
       let advance _ = (MatitaScript.instance ())#advance (); cursor () in
       let retract _ = (MatitaScript.instance ())#retract (); cursor () in
       let top _ = (MatitaScript.instance ())#goto `Top (); cursor () in
       let bottom _ = (MatitaScript.instance ())#goto `Bottom (); cursor () in
       let jump _ = (MatitaScript.instance ())#goto `Cursor (); cursor () in
-      let advance = locker advance in
-      let retract = locker retract in
-      let top = locker top in
-      let bottom = locker bottom in
-      let jump = locker jump in
+      let advance = locker (keep_focus advance) in
+      let retract = locker (keep_focus retract) in
+      let top = locker (keep_focus top) in
+      let bottom = locker (keep_focus bottom) in
+      let jump = locker (keep_focus jump) in
       let connect_key sym f =
         connect_key self#main#mainWinEventBox#event
           ~modifiers:[`CONTROL] ~stop:true sym f;