+ (** unicode handling *)
+ method nextSimilarSymbol =
+ let write_similarsymbol s =
+ let s = Glib.Utf8.from_unichar s in
+ let iter = source_view#source_buffer#get_iter_at_mark `INSERT in
+ assert(Glib.Utf8.validate s);
+ source_view#source_buffer#delete ~start:iter ~stop:(iter#copy#backward_chars 1);
+ source_view#source_buffer#insert ~iter:(source_view#source_buffer#get_iter_at_mark `INSERT) s;
+ (try source_view#source_buffer#delete_mark similarsymbols_tag
+ with GText.No_such_mark _ -> ());
+ ignore(source_view#source_buffer#create_mark ~name:similarsymbols_tag_name
+ (source_view#source_buffer#get_iter_at_mark `INSERT));
+ in
+ let new_similarsymbol =
+ try
+ let iter_ins = source_view#source_buffer#get_iter_at_mark `INSERT in
+ let iter_lig = source_view#source_buffer#get_iter_at_mark similarsymbols_tag in
+ not (iter_ins#equal iter_lig)
+ with GText.No_such_mark _ -> true
+ in
+ if new_similarsymbol then
+ (if not(self#expand_virtual_if_any (source_view#source_buffer#get_iter_at_mark `INSERT) "")then
+ let last_symbol =
+ let i = source_view#source_buffer#get_iter_at_mark `INSERT in
+ Glib.Utf8.first_char (i#get_slice ~stop:(i#copy#backward_chars 1))
+ in
+ (match Virtuals.similar_symbols last_symbol with
+ | [] -> ()
+ | eqclass ->
+ similarsymbols_orig <- eqclass;
+ let is_used =
+ try Hashtbl.find similar_memory similarsymbols_orig
+ with Not_found ->
+ let is_used = List.map (fun x -> x,false) eqclass in
+ Hashtbl.add similar_memory eqclass is_used;
+ is_used
+ in
+ let hd, next, tl =
+ let used, unused =
+ List.partition (fun s -> List.assoc s is_used) eqclass
+ in
+ match used @ unused with a::b::c -> a,b,c | _ -> assert false
+ in
+ let hd, tl =
+ if hd = last_symbol then next, tl @ [hd] else hd, (next::tl)
+ in
+ old_used_memory <- List.assoc hd is_used;
+ let is_used =
+ (hd,true) :: List.filter (fun (x,_) -> x <> hd) is_used
+ in
+ Hashtbl.replace similar_memory similarsymbols_orig is_used;
+ write_similarsymbol hd;
+ similarsymbols <- tl @ [ hd ]))
+ else
+ match similarsymbols with
+ | [] -> ()
+ | hd :: tl ->
+ let is_used = Hashtbl.find similar_memory similarsymbols_orig in
+ let last = HExtlib.list_last tl in
+ let old_used_for_last = old_used_memory in
+ old_used_memory <- List.assoc hd is_used;
+ let is_used =
+ (hd, true) :: (last,old_used_for_last) ::
+ List.filter (fun (x,_) -> x <> last && x <> hd) is_used
+ in
+ Hashtbl.replace similar_memory similarsymbols_orig is_used;
+ similarsymbols <- tl @ [ hd ];
+ write_similarsymbol hd
+
+ method private reset_similarsymbols =
+ similarsymbols <- [];
+ similarsymbols_orig <- [];
+ try source_view#source_buffer#delete_mark similarsymbols_tag
+ with GText.No_such_mark _ -> ()
+
+ method private expand_virtual_if_any iter tok =
+ try
+ let len = MatitaGtkMisc.utf8_string_length tok in
+ let last_word =
+ let prev = iter#copy#backward_chars len in
+ prev#get_slice ~stop:(prev#copy#backward_find_char
+ (fun x -> Glib.Unichar.isspace x || x = Glib.Utf8.first_char "\\"))
+ in
+ let inplaceof, symb = Virtuals.symbol_of_virtual last_word in
+ self#reset_similarsymbols;
+ let s = Glib.Utf8.from_unichar symb in
+ assert(Glib.Utf8.validate s);
+ source_view#source_buffer#delete ~start:iter
+ ~stop:(iter#copy#backward_chars
+ (MatitaGtkMisc.utf8_string_length inplaceof + len));
+ source_view#source_buffer#insert ~iter
+ (if inplaceof.[0] = '\\' then s else (s ^ tok));
+ true
+ with Virtuals.Not_a_virtual -> false
+
+ (** selections / clipboards handling *)
+
+ method markupSelected = MatitaMathView.has_selection ()
+ method private textSelected =
+ (source_view#source_buffer#get_iter_at_mark `INSERT)#compare
+ (source_view#source_buffer#get_iter_at_mark `SEL_BOUND) <> 0
+ method private markupStored = MatitaMathView.has_clipboard ()
+ method private textStored = clipboard#text <> None
+ method canCopy = self#textSelected
+ method canCut = self#textSelected
+ method canDelete = self#textSelected
+ (*CSC: WRONG CODE: we should look in the clipboard instead! *)
+ method canPaste = self#markupStored || self#textStored
+ method canPastePattern = self#markupStored
+
+ method safe_undo =
+ (* phase 1: we save the actual status of the marks and we undo *)
+ let locked_mark = `MARK (self#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;
+ self#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 ()
+
+ method safe_redo =
+ (* phase 1: we save the actual status of the marks, we redo and
+ we undo *)
+ let locked_mark = `MARK (self#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;
+ self#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 ()
+
+
+ method copy () =
+ if self#textSelected
+ then begin
+ MatitaMathView.empty_clipboard ();
+ source_view#buffer#copy_clipboard clipboard;
+ end else
+ MatitaMathView.copy_selection ()
+
+ method cut () =
+ source_view#buffer#cut_clipboard clipboard;
+ MatitaMathView.empty_clipboard ()
+
+ method delete () =
+ ignore (source_view#buffer#delete_selection ())
+
+ method paste () =
+ if MatitaMathView.has_clipboard ()
+ then source_view#buffer#insert (MatitaMathView.paste_clipboard `Term)
+ else source_view#buffer#paste_clipboard clipboard;
+ self#clean_dirty_lock
+
+ method pastePattern () =
+ source_view#buffer#insert (MatitaMathView.paste_clipboard `Pattern)
+