- let safe_undo =
- fun () ->
- (* phase 1: we save the actual status of the marks and we undo *)
- let locked_mark = `MARK ((MatitaScript.current ())#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.current ())#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.current ())#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.current ())#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
- connect_menu_item main#undoMenuItem safe_undo;
-(*CSC: XXX
- ignore(source_view#source_buffer#connect#can_undo
- ~callback:main#undoMenuItem#misc#set_sensitive);
-*) main#undoMenuItem#misc#set_sensitive true;
- connect_menu_item main#redoMenuItem safe_redo;
-(*CSC: XXX
- ignore(source_view#source_buffer#connect#can_redo
- ~callback:main#redoMenuItem#misc#set_sensitive);
-*) main#redoMenuItem#misc#set_sensitive true;
- 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] ->
- List.iter menu#remove [ copy; cut; delete; paste ];
- undo,redo
- | _ -> assert false in
- let add_menu_item =
- let i = ref 2 in (* last occupied position *)
- fun ?label ?stock () ->
- incr i;
- GMenu.image_menu_item ?label ?stock ~packing:(menu#insert ~pos:!i)
- ()
- in
- let copy = add_menu_item ~stock:`COPY () in
- let cut = add_menu_item ~stock:`CUT () in
- let delete = add_menu_item ~stock:`DELETE () in
- let paste = add_menu_item ~stock:`PASTE () in
- let paste_pattern = add_menu_item ~label:"Paste as pattern" () in
- copy#misc#set_sensitive self#canCopy;
- cut#misc#set_sensitive self#canCut;
- delete#misc#set_sensitive self#canDelete;
- paste#misc#set_sensitive self#canPaste;
- paste_pattern#misc#set_sensitive self#canPastePattern;
- connect_menu_item copy self#copy;
- connect_menu_item cut self#cut;
- connect_menu_item delete self#delete;
- connect_menu_item paste self#paste;
- connect_menu_item paste_pattern self#pastePattern;
- 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);
- connect_menu_item new_undoMenuItem 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);
- connect_menu_item new_redoMenuItem safe_redo));
-