- ignore(MatitaMathView.cicBrowser ()));
- connect_menu_item main#increaseFontSizeMenuItem (fun () ->
- self#increaseFontSize ();
- MatitaMathView.increase_font_size ();
- MatitaMathView.update_font_sizes ());
- connect_menu_item main#decreaseFontSizeMenuItem (fun () ->
- self#decreaseFontSize ();
- MatitaMathView.decrease_font_size ();
- MatitaMathView.update_font_sizes ());
- connect_menu_item main#normalFontSizeMenuItem (fun () ->
- self#resetFontSize ();
- MatitaMathView.reset_font_size ();
- MatitaMathView.update_font_sizes ());
- MatitaMathView.reset_font_size ();
-
- (** selections / clipboards handling *)
-
- method markupSelected = MatitaMathView.has_selection ()
- method private textSelected =
- (source_buffer#get_iter_at_mark `INSERT)#compare
- (source_buffer#get_iter_at_mark `SEL_BOUND) <> 0
- method private somethingSelected = self#markupSelected || self#textSelected
- method private markupStored = MatitaMathView.has_clipboard ()
- method private textStored = clipboard#text <> None
- method private somethingStored = self#markupStored || self#textStored
-
- method canCopy = self#somethingSelected
- method canCut = self#textSelected
- method canDelete = self#textSelected
- method canPaste = self#somethingStored
- method canPastePattern = self#markupStored
-
- 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;
- (MatitaScript.current ())#clean_dirty_lock
- method pastePattern () =
- source_view#buffer#insert (MatitaMathView.paste_clipboard `Pattern)
-
- 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_buffer#delete ~start:iter
- ~stop:(iter#copy#backward_chars
- (MatitaGtkMisc.utf8_string_length inplaceof + len));
- source_buffer#insert ~iter
- (if inplaceof.[0] = '\\' then s else (s ^ tok));
- true
- with Virtuals.Not_a_virtual -> false
-
- val similar_memory = Hashtbl.create 97
- val mutable old_used_memory = false
-
- method private nextSimilarSymbol () =
- let write_similarsymbol s =
- let s = Glib.Utf8.from_unichar s in
- let iter = source_buffer#get_iter_at_mark `INSERT in
- assert(Glib.Utf8.validate s);
- source_buffer#delete ~start:iter ~stop:(iter#copy#backward_chars 1);
- source_buffer#insert ~iter:(source_buffer#get_iter_at_mark `INSERT) s;
- (try source_buffer#delete_mark similarsymbols_tag
- with GText.No_such_mark _ -> ());
- ignore(source_buffer#create_mark ~name:similarsymbols_tag_name
- (source_buffer#get_iter_at_mark `INSERT));
- in
- let new_similarsymbol =
- try
- let iter_ins = source_buffer#get_iter_at_mark `INSERT in
- let iter_lig = 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_buffer#get_iter_at_mark `INSERT) "")then
- let last_symbol =
- let i = 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