X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaGui.ml;h=90826e98f9f6e72265313c65495798849b5913a3;hb=de4be1b51749200158ffb1984d6da3004b3690a9;hp=1d433f848a2f988dd42cde1c313c5048abbc15ad;hpb=ecd0ab19b82f611974bd76f3c740c842f566009d;p=helm.git

diff --git a/helm/matita/matitaGui.ml b/helm/matita/matitaGui.ml
index 1d433f848..90826e98f 100644
--- a/helm/matita/matitaGui.ml
+++ b/helm/matita/matitaGui.ml
@@ -107,7 +107,6 @@ let ask_unsaved parent =
 class gui () =
     (* creation order _is_ relevant for windows placement *)
   let main = new mainWin () in
-  let about = new aboutWin () in
   let fileSel = new fileSelectionWin () in
   let findRepl = new findReplWin () in
   let develList = new develListWin () in
@@ -142,7 +141,7 @@ class gui () =
         (* glade's check widgets *)
       List.iter (fun w -> w#check_widgets ())
         (let c w = (w :> <check_widgets: unit -> unit>) in
-        [ c about; c fileSel; c main; c findRepl]);
+        [ c fileSel; c main; c findRepl]);
         (* key bindings *)
       List.iter (* global key bindings *)
         (fun (key, callback) -> self#addKeyBinding key callback)
@@ -154,13 +153,33 @@ class gui () =
 *)
         [ ];
         (* about win *)
-      ignore (about#aboutWin#event#connect#delete (fun _ -> true));
-      ignore (main#aboutMenuItem#connect#activate (fun _ ->
-        about#aboutWin#show ()));
-      connect_button about#aboutDismissButton (fun _ ->
-        about#aboutWin#misc#hide ());
-      about#aboutLabel#set_label (Pcre.replace ~pat:"@VERSION@"
-        ~templ:BuildTimeConf.version about#aboutLabel#label);
+      let parse_txt_file file =
+       let ch = open_in file in
+       let l_rev = ref [] in
+       try
+        while true do
+         l_rev := input_line ch :: !l_rev;
+        done;
+        assert false
+       with
+        End_of_file ->
+         close_in ch;
+         List.rev !l_rev in 
+      let about_dialog =
+       GWindow.about_dialog
+        ~authors:(parse_txt_file "AUTHORS")
+        ~comments:"comments"
+        ~copyright:"Copyright (C) 2005, the HELM team"
+        ~license:(String.concat "\n" (parse_txt_file "LICENSE"))
+        (*?logo:GdkPixbuf.pixbuf*)
+        (*?logo_icon_name:string*)
+        ~name:"Matita"
+        ~version:BuildTimeConf.version
+        ~website:"http://helm.cs.unibo.it"
+        ()
+      in
+      ignore (main#aboutMenuItem#connect#activate
+       (fun _ -> about_dialog#present ()));
         (* findRepl win *)
       let show_find_Repl () = 
         findRepl#toplevel#misc#show ();
@@ -170,7 +189,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
@@ -196,9 +216,148 @@ class gui () =
       connect_button findRepl#cancelButton (fun _ -> hide_find_Repl ());
       ignore(findRepl#toplevel#event#connect#delete 
         ~callback:(fun _ -> hide_find_Repl ();true));
+      let safe_undo =
+       fun () ->
+        (* phase 1: we save the actual status of the marks and we undo *)
+        let locked_mark = `MARK ((MatitaScript.instance ())#locked_mark) in
+        let locked_iter = source_view#buffer#get_iter_at_mark locked_mark in
+        let locked_iter_offset = locked_iter#offset in
+        let mark2 =
+         `MARK
+           (source_view#buffer#create_mark ~name:"lock_point"
+             ~left_gravity:true locked_iter) in
+        source_view#source_buffer#undo ();
+        (* phase 2: we save the cursor position and we redo, restoring
+           the previous status of all the marks *)
+        let cursor_iter = source_view#buffer#get_iter_at_mark `INSERT in
+        let mark =
+         `MARK
+           (source_view#buffer#create_mark ~name:"undo_point"
+             ~left_gravity:true cursor_iter)
+        in
+         source_view#source_buffer#redo ();
+         let mark_iter = source_view#buffer#get_iter_at_mark mark in
+         let mark2_iter = source_view#buffer#get_iter_at_mark mark2 in
+         let mark2_iter = mark2_iter#set_offset locked_iter_offset in
+          source_view#buffer#move_mark locked_mark ~where:mark2_iter;
+          source_view#buffer#delete_mark mark;
+          source_view#buffer#delete_mark mark2;
+          (* phase 3: if after the undo the cursor was in the locked area,
+             then we move it there again and we perform a goto *)
+          if mark_iter#offset < locked_iter_offset then
+           begin
+            source_view#buffer#move_mark `INSERT ~where:mark_iter;
+            (MatitaScript.instance ())#goto `Cursor ();
+           end;
+          (* phase 4: we perform again the undo. This time we are sure that
+             the text to undo is not locked *)
+          source_view#source_buffer#undo ();
+          source_view#misc#grab_focus () in
+      let safe_redo =
+       fun () ->
+        (* phase 1: we save the actual status of the marks, we redo and
+           we undo *)
+        let locked_mark = `MARK ((MatitaScript.instance ())#locked_mark) in
+        let locked_iter = source_view#buffer#get_iter_at_mark locked_mark in
+        let locked_iter_offset = locked_iter#offset in
+        let mark2 =
+         `MARK
+           (source_view#buffer#create_mark ~name:"lock_point"
+             ~left_gravity:true locked_iter) in
+        source_view#source_buffer#redo ();
+        source_view#source_buffer#undo ();
+        (* phase 2: we save the cursor position and we restore
+           the previous status of all the marks *)
+        let cursor_iter = source_view#buffer#get_iter_at_mark `INSERT in
+        let mark =
+         `MARK
+           (source_view#buffer#create_mark ~name:"undo_point"
+             ~left_gravity:true cursor_iter)
+        in
+         let mark_iter = source_view#buffer#get_iter_at_mark mark in
+         let mark2_iter = source_view#buffer#get_iter_at_mark mark2 in
+         let mark2_iter = mark2_iter#set_offset locked_iter_offset in
+          source_view#buffer#move_mark locked_mark ~where:mark2_iter;
+          source_view#buffer#delete_mark mark;
+          source_view#buffer#delete_mark mark2;
+          (* phase 3: if after the undo the cursor is in the locked area,
+             then we move it there again and we perform a goto *)
+          if mark_iter#offset < locked_iter_offset then
+           begin
+            source_view#buffer#move_mark `INSERT ~where:mark_iter;
+            (MatitaScript.instance ())#goto `Cursor ();
+           end;
+          (* phase 4: we perform again the redo. This time we are sure that
+             the text to redo is not locked *)
+          source_view#source_buffer#redo ();
+          source_view#misc#grab_focus ()
+      in
+      ignore(self#main#undoMenuItem#connect#activate ~callback:safe_undo);
+      ignore(source_view#source_buffer#connect#can_undo
+        ~callback:self#main#undoMenuItem#misc#set_sensitive);
+      ignore(self#main#redoMenuItem#connect#activate ~callback:safe_redo);
+      ignore(source_view#source_buffer#connect#can_redo
+        ~callback:self#main#redoMenuItem#misc#set_sensitive);
+      ignore(source_view#connect#after#populate_popup
+       ~callback:(fun pre_menu ->
+         let menu = new GMenu.menu pre_menu in
+         let menuItems = menu#children in
+         let undoMenuItem, redoMenuItem =
+          match menuItems with
+             [undo;redo;sep1;cut;copy;paste;delete;sep2;
+              selectall;sep3;inputmethod;insertunicodecharacter] -> undo,redo
+           | _ -> assert false in
+         let new_undoMenuItem =
+          GMenu.image_menu_item
+           ~image:(GMisc.image ~stock:`UNDO ())
+           ~use_mnemonic:true
+           ~label:"_Undo"
+           ~packing:(menu#insert ~pos:0) () in
+         new_undoMenuItem#misc#set_sensitive
+          (undoMenuItem#misc#get_flag `SENSITIVE);
+         menu#remove (undoMenuItem :> GMenu.menu_item);
+         ignore(new_undoMenuItem#connect#activate ~callback:safe_undo);
+         let new_redoMenuItem =
+          GMenu.image_menu_item
+           ~image:(GMisc.image ~stock:`REDO ())
+           ~use_mnemonic:true
+           ~label:"_Redo"
+           ~packing:(menu#insert ~pos:1) () in
+         new_redoMenuItem#misc#set_sensitive
+          (redoMenuItem#misc#get_flag `SENSITIVE);
+          menu#remove (redoMenuItem :> GMenu.menu_item);
+          ignore(new_redoMenuItem#connect#activate ~callback:safe_redo);
+         ));
+      let clipboard =
+       let atom = Gdk.Atom.clipboard in
+        GData.clipboard atom in
+      ignore(self#main#cutMenuItem#connect#activate
+        ~callback:(fun () -> source_view#buffer#cut_clipboard clipboard));
+      ignore(self#main#copyMenuItem#connect#activate
+        ~callback:(fun () -> source_view#buffer#copy_clipboard clipboard));
+      ignore(self#main#pasteMenuItem#connect#activate
+        ~callback:(fun () ->
+          source_view#buffer#paste_clipboard clipboard;
+          (MatitaScript.instance ())#clean_dirty_lock));
+      ignore(self#main#deleteMenuItem#connect#activate
+        ~callback:(fun () -> ignore (source_view#buffer#delete_selection ())));
       ignore(self#main#findReplMenuItem#connect#activate
         ~callback:show_find_Repl);
       ignore (findRepl#findEntry#connect#activate ~callback:find_forward);
+        (* interface lockers *)
+      let lock_world _ =
+        main#buttonsToolbar#misc#set_sensitive false;
+        source_view#set_editable false
+      in
+      let unlock_world _ =
+        main#buttonsToolbar#misc#set_sensitive true;
+        source_view#set_editable true
+      in
+      let locker f = 
+        fun () -> 
+          lock_world ();
+          try f ();unlock_world () with exc -> unlock_world (); raise exc
+      in
         (* developments win *)
       let model = 
         new MatitaGtkMisc.multiStringListModel 
@@ -234,12 +393,20 @@ class gui () =
         (fun () -> 
           match get_devel_selected () with
           | None -> ()
-          | Some d -> ignore(MatitamakeLib.build_development_in_bg refresh d));
+          | Some d -> 
+              let build = locker 
+                (fun () -> MatitamakeLib.build_development_in_bg refresh d)
+              in
+              ignore(build ()));
       connect_button develList#cleanButton 
         (fun () -> 
           match get_devel_selected () with
           | None -> ()
-          | Some d -> ignore(MatitamakeLib.clean_development_in_bg refresh d));
+          | Some d -> 
+              let clean = locker 
+                (fun () -> MatitamakeLib.clean_development_in_bg refresh d)
+              in
+              ignore(clean ()));
       connect_button develList#closeButton 
         (fun () -> develList#toplevel#misc#hide());
       ignore(develList#toplevel#event#connect#delete 
@@ -429,15 +596,19 @@ class gui () =
           | Some f -> 
                 script#reset (); 
                 script#assignFileName f;
+                source_view#source_buffer#begin_not_undoable_action ();
                 script#loadFromFile (); 
+                source_view#source_buffer#end_not_undoable_action ();
                 console#message ("'"^f^"' loaded.\n");
                 self#_enableSaveTo f
           | None -> ()
         with MatitaTypes.Cancel -> ()
       in
       let newScript () = 
+        source_view#source_buffer#begin_not_undoable_action ();
         (s ())#reset (); 
         (s ())#template (); 
+        source_view#source_buffer#end_not_undoable_action ();
         disableSave ();
         script_fname <- None
       in
@@ -445,24 +616,11 @@ class gui () =
         source_buffer#place_cursor
           (source_buffer#get_iter_at_mark (`NAME "locked"))
       in
-      let lock_world _ =
-        main#buttonsToolbar#misc#set_sensitive false;
-        source_view#set_editable false
-      in
-      let unlock_world _ =
-        main#buttonsToolbar#misc#set_sensitive true;
-        source_view#set_editable true
-      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 locker f = 
-        fun () -> 
-          lock_world ();
-          try f ();unlock_world () with exc -> unlock_world (); raise exc
-      in
       let advance = locker advance in
       let retract = locker retract in
       let top = locker top in
@@ -562,7 +720,9 @@ class gui () =
           output_string oc template;
           close_out oc
         end;
+      source_view#source_buffer#begin_not_undoable_action ();
       script#loadFromFile ();
+      source_view#source_buffer#end_not_undoable_action ();
       console#message ("'"^file^"' loaded.");
       self#_enableSaveTo file
       
@@ -580,7 +740,6 @@ class gui () =
 
     method console = console
     method sourceView: GSourceView.source_view = (source_view: GSourceView.source_view)
-    method about = about
     method fileSel = fileSel
     method findRepl = findRepl
     method main = main