From f3d0ba1e75bc3383d766f3a33a19352db19854df Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Mon, 20 Dec 2010 17:24:55 +0000 Subject: [PATCH] Large commit: refactoring of the code of the interface. 1. management of font sizes centralized in MatitaMisc according to the MVC paradigm 2. functionalities related to the script window moved from MatitaGui to MatitaScript --- matita/matita/cicMathView.ml | 19 +- matita/matita/cicMathView.mli | 3 - matita/matita/matita.ml | 9 +- matita/matita/matitaGui.ml | 584 +++++++------------------------ matita/matita/matitaGuiTypes.mli | 23 -- matita/matita/matitaMathView.ml | 8 - matita/matita/matitaMathView.mli | 1 - matita/matita/matitaMisc.ml | 18 +- matita/matita/matitaMisc.mli | 7 +- matita/matita/matitaScript.ml | 346 +++++++++++++++++- matita/matita/matitaScript.mli | 28 +- 11 files changed, 516 insertions(+), 530 deletions(-) diff --git a/matita/matita/cicMathView.ml b/matita/matita/cicMathView.ml index ea7fd5160..2fe7db06b 100644 --- a/matita/matita/cicMathView.ml +++ b/matita/matita/cicMathView.ml @@ -40,9 +40,6 @@ class type cicMathView = object inherit GObj.widget - method set_font_size: int -> unit - method update_font_size: unit - method load_root : root:document_element -> unit method remove_selections: unit method set_selection: document_element option -> unit @@ -182,9 +179,6 @@ object (self) inherit GSourceView2.source_view obj method strings_of_selection = (assert false : (paste_kind * string) list) - method update_font_size = - self#misc#modify_font_by_name - (sprintf "%s %d" BuildTimeConf.script_font (MatitaMisc.get_current_font_size ())) method set_href_callback = (function _ -> () : (string -> unit) option -> unit) method private set_cic_info = (function _ -> () : unit (*(Cic.conjecture option * (Cic.id, Cic.term) Hashtbl.t * (Cic.id, Cic.hypothesis) Hashtbl.t * @@ -198,15 +192,15 @@ object (self) method remove_selections = (() : unit) method set_selection = (fun _ -> () : document_element option -> unit) method get_selections = (assert false : document_element list) - method set_font_size font_size = - self#misc#modify_font_by_name - (sprintf "%s %d" BuildTimeConf.script_font font_size) initializer - self#set_font_size (MatitaMisc.get_current_font_size ()); self#source_buffer#set_language (Some MatitaGtkMisc.matita_lang); self#source_buffer#set_highlight_syntax true; - self#set_editable false + self#set_editable false; + MatitaMisc.observe_font_size + (fun size -> + self#misc#modify_font_by_name + (sprintf "%s %d" BuildTimeConf.script_font size)) (* MATITA1.0 inherit GMathViewAux.multi_selection_math_view obj @@ -223,7 +217,6 @@ object (self) val maction_cursor = Gdk.Cursor.create `QUESTION_ARROW initializer - self#set_font_size (MatitaMisc.get_current_font_size ()); ignore (self#connect#selection_changed self#choose_selection_cb); ignore (self#event#connect#button_press self#button_press_cb); ignore (self#event#connect#button_release self#button_release_cb); @@ -448,8 +441,6 @@ object (self) | None -> self#set_selection None); selection_changed <- true - method update_font_size = self#set_font_size (MatitaMisc.get_current_font_size ()) - (** find a term by id from stored CIC infos @return either `Hyp if the id * correspond to an hypothesis or `Term (cic, hyp) if the id correspond to a * term. In the latter case hyp is either None (if the term is a subterm of diff --git a/matita/matita/cicMathView.mli b/matita/matita/cicMathView.mli index bb95b3ef7..8f252a967 100644 --- a/matita/matita/cicMathView.mli +++ b/matita/matita/cicMathView.mli @@ -29,9 +29,6 @@ class type cicMathView = object inherit GObj.widget - method set_font_size: int -> unit - method update_font_size: unit - method load_root : root:document_element -> unit method remove_selections: unit method set_selection: document_element option -> unit diff --git a/matita/matita/matita.ml b/matita/matita/matita.ml index ee20eda89..c2cc81f66 100644 --- a/matita/matita/matita.ml +++ b/matita/matita/matita.ml @@ -49,14 +49,13 @@ let gui = MatitaGui.instance () let script = let s = MatitaScript.script - ~source_view:gui#sourceView - ~urichooser:(fun uris -> + ~urichooser:(fun source_view uris -> try MatitaGui.interactive_uri_choice ~selection_mode:`SINGLE ~title:"Matita: URI chooser" ~msg:"Select the URI" ~hide_uri_entry:true ~hide_try:true ~ok_label:"_Apply" ~ok_action:`SELECT - ~copy_cb:(fun s -> gui#sourceView#buffer#insert ("\n"^s^"\n")) + ~copy_cb:(fun s -> source_view#buffer#insert ("\n"^s^"\n")) () ~id:"boh?" uris with MatitaTypes.Cancel -> []) ~ask_confirmation: @@ -67,10 +66,6 @@ let script = in Predefined_virtuals.load_predefined_virtuals (); Predefined_virtuals.load_predefined_classes (); - gui#sourceView#source_buffer#begin_not_undoable_action (); - s#reset (); - s#template (); - gui#sourceView#source_buffer#end_not_undoable_action (); s (* math viewers *) diff --git a/matita/matita/matitaGui.ml b/matita/matita/matitaGui.ml index 7589f19f8..5217abeb2 100644 --- a/matita/matita/matitaGui.ml +++ b/matita/matita/matitaGui.ml @@ -191,7 +191,7 @@ class interpErrorModel = exception UseLibrary;; -let rec interactive_error_interp ~all_passes +let interactive_error_interp ~all_passes (source_buffer:GSourceView2.source_buffer) notify_exn offset errorll filename = (* hook to save a script for each disambiguation error *) @@ -342,16 +342,6 @@ let rec interactive_error_interp ~all_passes GtkThread.main () -(** Selection handling - * Two clipboards are used: "clipboard" and "primary". - * "primary" is used by X, when you hit the middle button mouse is content is - * pasted between applications. In Matita this selection always contain the - * textual version of the selected term. - * "clipboard" is used inside Matita only and support ATM two different targets: - * "TERM" and "PATTERN", in the future other targets like "MATHMLCONTENT" may - * be added - *) - class gui () = (* creation order _is_ relevant for windows placement *) let main = new mainWin () in @@ -361,38 +351,12 @@ class gui () = [ main#mainWinEventBox ] in let console = new console ~buffer:main#logTextView#buffer () in - let (source_view: GSourceView2.source_view) = - GSourceView2.source_view - ~auto_indent:true - ~insert_spaces_instead_of_tabs:true ~tab_width:2 - ~right_margin_position:80 ~show_right_margin:true - ~smart_home_end:`AFTER - ~packing:main#scriptScrolledWin#add - () - in - let default_font_size = - Helm_registry.get_opt_default Helm_registry.int - ~default:BuildTimeConf.default_font_size "matita.font_size" - in - let similarsymbols_tag_name = "similarsymbolos" in - let similarsymbols_tag = `NAME similarsymbols_tag_name in - let source_buffer = source_view#source_buffer in + let source_view () = (MatitaScript.current ())#source_view in object (self) val mutable chosen_file = None val mutable _ok_not_exists = false val mutable _only_directory = false - val mutable font_size = default_font_size - val mutable similarsymbols = [] - val mutable similarsymbols_orig = [] - val clipboard = GData.clipboard Gdk.Atom.clipboard - val primary = GData.clipboard Gdk.Atom.primary - method private reset_similarsymbols = - similarsymbols <- []; - similarsymbols_orig <- []; - try source_buffer#delete_mark similarsymbols_tag - with GText.No_such_mark _ -> () - initializer let s () = MatitaScript.current () in (* glade's check widgets *) @@ -456,28 +420,30 @@ class gui () = in let hide_find_Repl () = findRepl#toplevel#misc#hide () in let find_forward _ = + let source_view = source_view () in let highlight start end_ = - source_buffer#move_mark `INSERT ~where:start; - source_buffer#move_mark `SEL_BOUND ~where:end_; + source_view#source_buffer#move_mark `INSERT ~where:start; + source_view#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 + let iter = source_view#source_buffer#get_iter `SEL_BOUND in match iter#forward_search text with | None -> - (match source_buffer#start_iter#forward_search text with + (match source_view#source_buffer#start_iter#forward_search text with | None -> () | Some (start,end_) -> highlight start end_) | Some (start,end_) -> highlight start end_ in let replace _ = + let source_view = source_view () in let text = findRepl#replaceEntry#text in - let ins = source_buffer#get_iter `INSERT in - let sel = source_buffer#get_iter `SEL_BOUND in + let ins = source_view#source_buffer#get_iter `INSERT in + let sel = source_view#source_buffer#get_iter `SEL_BOUND in if ins#compare sel < 0 then begin - ignore(source_buffer#delete_selection ()); - source_buffer#insert text + ignore(source_view#source_buffer#delete_selection ()); + source_view#source_buffer#insert text end in connect_button findRepl#findButton find_forward; @@ -485,175 +451,57 @@ 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.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; + connect_menu_item main#undoMenuItem + (fun () -> (MatitaScript.current ())#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; + connect_menu_item main#redoMenuItem + (fun () -> (MatitaScript.current ())#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)); - connect_menu_item main#editMenu (fun () -> - main#copyMenuItem#misc#set_sensitive self#canCopy; - main#cutMenuItem#misc#set_sensitive self#canCut; - main#deleteMenuItem#misc#set_sensitive self#canDelete; - main#pasteMenuItem#misc#set_sensitive self#canPaste; - main#pastePatternMenuItem#misc#set_sensitive self#canPastePattern); - connect_menu_item main#copyMenuItem self#copy; - connect_menu_item main#cutMenuItem self#cut; - connect_menu_item main#deleteMenuItem self#delete; - connect_menu_item main#pasteMenuItem self#paste; - connect_menu_item main#pastePatternMenuItem self#pastePattern; + main#copyMenuItem#misc#set_sensitive + (MatitaScript.current ())#canCopy; + main#cutMenuItem#misc#set_sensitive + (MatitaScript.current ())#canCut; + main#deleteMenuItem#misc#set_sensitive + (MatitaScript.current ())#canDelete; + main#pasteMenuItem#misc#set_sensitive + (MatitaScript.current ())#canPaste; + main#pastePatternMenuItem#misc#set_sensitive + (MatitaScript.current ())#canPastePattern); + connect_menu_item main#copyMenuItem + (fun () -> (MatitaScript.current ())#copy ()); + connect_menu_item main#cutMenuItem + (fun () -> (MatitaScript.current ())#cut ()); + connect_menu_item main#deleteMenuItem + (fun () -> (MatitaScript.current ())#delete ()); + connect_menu_item main#pasteMenuItem + (fun () -> (MatitaScript.current ())#paste ()); + connect_menu_item main#pastePatternMenuItem + (fun () -> (MatitaScript.current ())#pastePattern ()); connect_menu_item main#selectAllMenuItem (fun () -> - source_buffer#move_mark `INSERT source_buffer#start_iter; - source_buffer#move_mark `SEL_BOUND source_buffer#end_iter); + let source_view = source_view () in + source_view#source_buffer#move_mark `INSERT source_view#source_buffer#start_iter; + source_view#source_buffer#move_mark `SEL_BOUND source_view#source_buffer#end_iter); connect_menu_item main#findReplMenuItem show_find_Repl; connect_menu_item main#externalEditorMenuItem self#externalEditor; - connect_menu_item main#ligatureButton self#nextSimilarSymbol; - ignore(source_buffer#connect#after#insert_text - ~callback:(fun iter str -> - if main#menuitemAutoAltL#active && (str = " " || str = "\n") then - ignore(self#expand_virtual_if_any iter str))); + connect_menu_item main#ligatureButton + (fun () -> (MatitaScript.current ())#nextSimilarSymbol); ignore (findRepl#findEntry#connect#activate find_forward); (* interface lockers *) let lock_world _ = + let source_view = source_view () in main#buttonsToolbar#misc#set_sensitive false; main#scriptMenu#misc#set_sensitive false; source_view#set_editable false in let unlock_world _ = + let source_view = source_view () in main#buttonsToolbar#misc#set_sensitive true; main#scriptMenu#misc#set_sensitive true; source_view#set_editable true; @@ -661,7 +509,7 @@ class gui () = GtkThread.sync (fun () -> ()) () in let worker_thread = ref None in - let notify_exn exn = + let notify_exn (source_view : GSourceView2.source_view) exn = let floc, msg = MatitaExcPp.to_string exn in begin match floc with @@ -672,56 +520,58 @@ class gui () = let locked_mark = script#locked_mark in let error_tag = script#error_tag in let baseoffset = - (source_buffer#get_iter_at_mark (`MARK locked_mark))#offset in + (source_view#source_buffer#get_iter_at_mark (`MARK locked_mark))#offset in let x' = baseoffset + x in let y' = baseoffset + y in - let x_iter = source_buffer#get_iter (`OFFSET x') in - let y_iter = source_buffer#get_iter (`OFFSET y') in - source_buffer#apply_tag error_tag ~start:x_iter ~stop:y_iter; + let x_iter = source_view#source_buffer#get_iter (`OFFSET x') in + let y_iter = source_view#source_buffer#get_iter (`OFFSET y') in + source_view#source_buffer#apply_tag error_tag ~start:x_iter ~stop:y_iter; let id = ref None in - id := Some (source_buffer#connect#changed ~callback:(fun () -> - source_buffer#remove_tag error_tag - ~start:source_buffer#start_iter - ~stop:source_buffer#end_iter; + id := Some (source_view#source_buffer#connect#changed ~callback:(fun () -> + source_view#source_buffer#remove_tag error_tag + ~start:source_view#source_buffer#start_iter + ~stop:source_view#source_buffer#end_iter; match !id with | None -> assert false (* a race condition occurred *) | Some id -> - (new GObj.gobject_ops source_buffer#as_buffer)#disconnect id)); - source_buffer#place_cursor - (source_buffer#get_iter (`OFFSET x')); + (new GObj.gobject_ops source_view#source_buffer#as_buffer)#disconnect id)); + source_view#source_buffer#place_cursor + (source_view#source_buffer#get_iter (`OFFSET x')); end; HLog.error msg in - let locker f () = + let locker f script = + let source_view = script#source_view in let thread_main = fun () -> lock_world (); let saved_use_library= !MultiPassDisambiguator.use_library in try MultiPassDisambiguator.use_library := !all_disambiguation_passes; - f (); + f script; MultiPassDisambiguator.use_library := saved_use_library; unlock_world () with | MultiPassDisambiguator.DisambiguationError (offset,errorll) -> (try interactive_error_interp - ~all_passes:!all_disambiguation_passes source_buffer - notify_exn offset errorll (s())#filename + ~all_passes:!all_disambiguation_passes source_view#source_buffer + (notify_exn source_view) offset errorll (s())#filename with | UseLibrary -> MultiPassDisambiguator.use_library := true; - (try f () + (try f script with | MultiPassDisambiguator.DisambiguationError (offset,errorll) -> - interactive_error_interp ~all_passes:true source_buffer - notify_exn offset errorll (s())#filename + interactive_error_interp ~all_passes:true source_view#source_buffer + (notify_exn source_view) offset errorll (s())#filename | exc -> - notify_exn exc); - | exc -> notify_exn exc); + notify_exn source_view exc); + | exc -> notify_exn source_view exc); MultiPassDisambiguator.use_library := saved_use_library; unlock_world () | exc -> - (try notify_exn exc with Sys.Break as e -> notify_exn e); + (try notify_exn source_view exc + with Sys.Break as e -> notify_exn source_view e); unlock_world () in (*thread_main ();*) @@ -746,12 +596,11 @@ class gui () = match !worker_thread with None -> assert false | Some t -> interrupt := Some (Thread.id t) in - let keep_focus f = - fun () -> + let keep_focus f (script: MatitaScript.script) = try - f (); source_view#misc#grab_focus () + f script; script#source_view#misc#grab_focus () with - exc -> source_view#misc#grab_focus (); raise exc in + exc -> script#source_view#misc#grab_focus (); raise exc in (* file selection win *) ignore (fileSel#fileSelectionWin#event#connect#delete (fun _ -> true)); @@ -794,48 +643,48 @@ class gui () = else main#tacticsButtonsHandlebox#misc#hide ()) ~check:main#menuitemPalette; connect_button main#butImpl_intro - (fun () -> source_buffer#insert "apply rule (⇒#i […] (…));\n"); + (fun () -> (source_view ())#source_buffer#insert "apply rule (⇒#i […] (…));\n"); connect_button main#butAnd_intro - (fun () -> source_buffer#insert + (fun () -> (source_view ())#source_buffer#insert "apply rule (∧#i (…) (…));\n\t[\n\t|\n\t]\n"); connect_button main#butOr_intro_left - (fun () -> source_buffer#insert "apply rule (∨#i_l (…));\n"); + (fun () -> (source_view ())#source_buffer#insert "apply rule (∨#i_l (…));\n"); connect_button main#butOr_intro_right - (fun () -> source_buffer#insert "apply rule (∨#i_r (…));\n"); + (fun () -> (source_view ())#source_buffer#insert "apply rule (∨#i_r (…));\n"); connect_button main#butNot_intro - (fun () -> source_buffer#insert "apply rule (¬#i […] (…));\n"); + (fun () -> (source_view ())#source_buffer#insert "apply rule (¬#i […] (…));\n"); connect_button main#butTop_intro - (fun () -> source_buffer#insert "apply rule (⊤#i);\n"); + (fun () -> (source_view ())#source_buffer#insert "apply rule (⊤#i);\n"); connect_button main#butImpl_elim - (fun () -> source_buffer#insert + (fun () -> (source_view ())#source_buffer#insert "apply rule (⇒#e (…) (…));\n\t[\n\t|\n\t]\n"); connect_button main#butAnd_elim_left - (fun () -> source_buffer#insert "apply rule (∧#e_l (…));\n"); + (fun () -> (source_view ())#source_buffer#insert "apply rule (∧#e_l (…));\n"); connect_button main#butAnd_elim_right - (fun () -> source_buffer#insert "apply rule (∧#e_r (…));\n"); + (fun () -> (source_view ())#source_buffer#insert "apply rule (∧#e_r (…));\n"); connect_button main#butOr_elim - (fun () -> source_buffer#insert + (fun () -> (source_view ())#source_buffer#insert "apply rule (∨#e (…) […] (…) […] (…));\n\t[\n\t|\n\t|\n\t]\n"); connect_button main#butNot_elim - (fun () -> source_buffer#insert + (fun () -> (source_view ())#source_buffer#insert "apply rule (¬#e (…) (…));\n\t[\n\t|\n\t]\n"); connect_button main#butBot_elim - (fun () -> source_buffer#insert "apply rule (⊥#e (…));\n"); + (fun () -> (source_view ())#source_buffer#insert "apply rule (⊥#e (…));\n"); connect_button main#butRAA - (fun () -> source_buffer#insert "apply rule (RAA […] (…));\n"); + (fun () -> (source_view ())#source_buffer#insert "apply rule (RAA […] (…));\n"); connect_button main#butUseLemma - (fun () -> source_buffer#insert "apply rule (lem #premises name …);\n"); + (fun () -> (source_view ())#source_buffer#insert "apply rule (lem #premises name …);\n"); connect_button main#butDischarge - (fun () -> source_buffer#insert "apply rule (discharge […]);\n"); + (fun () -> (source_view ())#source_buffer#insert "apply rule (discharge […]);\n"); connect_button main#butForall_intro - (fun () -> source_buffer#insert "apply rule (∀#i {…} (…));\n"); + (fun () -> (source_view ())#source_buffer#insert "apply rule (∀#i {…} (…));\n"); connect_button main#butForall_elim - (fun () -> source_buffer#insert "apply rule (∀#e {…} (…));\n"); + (fun () -> (source_view ())#source_buffer#insert "apply rule (∀#e {…} (…));\n"); connect_button main#butExists_intro - (fun () -> source_buffer#insert "apply rule (∃#i {…} (…));\n"); + (fun () -> (source_view ())#source_buffer#insert "apply rule (∃#i {…} (…));\n"); connect_button main#butExists_elim - (fun () -> source_buffer#insert + (fun () -> (source_view ())#source_buffer#insert "apply rule (∃#e (…) {…} […] (…));\n\t[\n\t|\n\t]\n"); @@ -868,13 +717,9 @@ class gui () = | MatitaScript.ActionCancelled s -> HLog.error s | exn -> if not (Helm_registry.get_bool "matita.debug") then - notify_exn exn + (*CSC: MatitaScript.current ??? *) + notify_exn (MatitaScript.current ())#source_view exn else raise exn); - (* script *) - let _ = - source_buffer#set_language (Some MatitaGtkMisc.matita_lang); - source_buffer#set_highlight_syntax true - in let disableSave () = (s())#assignFileName None; main#saveMenuItem#misc#set_sensitive false @@ -898,6 +743,7 @@ class gui () = else saveAsScript () in let abandon_script () = + let source_view = source_view () in let grafite_status = (s ())#grafite_status in if source_view#buffer#modified then (match ask_unsaved main#toplevel with @@ -907,6 +753,7 @@ class gui () = save_moo grafite_status in let loadScript () = + let source_view = source_view () in let script = s () in try match self#chooseFile () with @@ -925,6 +772,7 @@ class gui () = with MatitaTypes.Cancel -> () in let newScript () = + let source_view = source_view () in abandon_script (); source_view#source_buffer#begin_not_undoable_action (); (s ())#reset (); @@ -933,20 +781,22 @@ class gui () = disableSave () in let cursor () = - source_buffer#place_cursor - (source_buffer#get_iter_at_mark (`NAME "locked")) in - let advance _ = (MatitaScript.current ())#advance (); cursor () in - let retract _ = (MatitaScript.current ())#retract (); cursor () in - let top _ = (MatitaScript.current ())#goto `Top (); cursor () in - let bottom _ = (MatitaScript.current ())#goto `Bottom (); cursor () in - let jump _ = (MatitaScript.current ())#goto `Cursor (); cursor () 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 source_view = source_view () in + source_view#source_buffer#place_cursor + (source_view#source_buffer#get_iter_at_mark (`NAME "locked")) in + let advance (script: MatitaScript.script) = script#advance (); cursor () in + let retract (script: MatitaScript.script) = script#retract (); cursor () in + let top (script: MatitaScript.script) = script#goto `Top (); cursor () in + let bottom (script: MatitaScript.script) = script#goto `Bottom (); cursor () in + let jump (script: MatitaScript.script) = script#goto `Cursor (); cursor () in + let advance () = locker (keep_focus advance) (MatitaScript.current ()) in + let retract () = locker (keep_focus retract) (MatitaScript.current ()) in + let top () = locker (keep_focus top) (MatitaScript.current ()) in + let bottom () = locker (keep_focus bottom) (MatitaScript.current ()) in + let jump () = locker (keep_focus jump) (MatitaScript.current ()) in (* quit *) self#setQuitCallback (fun () -> +(*CSC: iterare su tutti gli script! let script = MatitaScript.current () in if source_view#buffer#modified then match ask_unsaved main#toplevel with @@ -958,7 +808,7 @@ class gui () = | `CANCEL -> () else (save_moo script#grafite_status; - GMain.Main.quit ())); + GMain.Main.quit ())*) assert false); connect_button main#scriptAdvanceButton advance; connect_button main#scriptRetractButton retract; connect_button main#scriptTopButton top; @@ -990,8 +840,6 @@ class gui () = (fun _ -> let c = MatitaMathView.cicBrowser () in c#load (`About `TeX)); - (* script monospace font stuff *) - self#updateFontSize (); (* debug menu *) main#debugMenu#misc#hide (); (* HBUGS *) @@ -1001,8 +849,6 @@ class gui () = main#hintMediumImage#set_file (image_path "matita-bulb-medium.png"); main#hintHighImage#set_file (image_path "matita-bulb-high.png"); *) - (* focus *) - self#sourceView#misc#grab_focus (); (* main win dimension *) let width = Gdk.Screen.width ~screen:(Gdk.Screen.default ()) () in let height = Gdk.Screen.height ~screen:(Gdk.Screen.default ()) () in @@ -1014,177 +860,18 @@ class gui () = let script_w = main_w * 6 / 10 in main#toplevel#resize ~width:main_w ~height:main_h; main#hpaneScriptSequent#set_position script_w; - (* source_view *) - ignore(source_view#connect#after#paste_clipboard - ~callback:(fun () -> (MatitaScript.current ())#clean_dirty_lock)); - (* clean_locked is set to true only "during" a PRIMARY paste - operation (i.e. by clicking with the second mouse button) *) - let clean_locked = ref false in - ignore(source_view#event#connect#button_press - ~callback: - (fun button -> - if GdkEvent.Button.button button = 2 then - clean_locked := true; - false - )); - ignore(source_view#event#connect#button_release - ~callback:(fun button -> clean_locked := false; false)); - ignore(source_view#buffer#connect#after#apply_tag - ~callback:( - fun tag ~start:_ ~stop:_ -> - if !clean_locked && - tag#get_oid = (MatitaScript.current ())#locked_tag#get_oid - then - begin - clean_locked := false; - (MatitaScript.current ())#clean_dirty_lock; - clean_locked := true - end)); (* math view handling *) connect_menu_item main#newCicBrowserMenuItem (fun () -> ignore(MatitaMathView.cicBrowser ())); - connect_menu_item main#increaseFontSizeMenuItem (fun () -> - self#increaseFontSize (); - MatitaMisc.increase_font_size (); - MatitaMathView.update_font_sizes ()); - connect_menu_item main#decreaseFontSizeMenuItem (fun () -> - self#decreaseFontSize (); - MatitaMisc.decrease_font_size (); - MatitaMathView.update_font_sizes ()); - connect_menu_item main#normalFontSizeMenuItem (fun () -> - self#resetFontSize (); - MatitaMisc.reset_font_size (); - MatitaMathView.update_font_sizes ()); - MatitaMisc.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 + connect_menu_item main#increaseFontSizeMenuItem + MatitaMisc.increase_font_size; + connect_menu_item main#decreaseFontSizeMenuItem + MatitaMisc.decrease_font_size; + connect_menu_item main#normalFontSizeMenuItem + MatitaMisc.reset_font_size; method private externalEditor () = + let source_view = source_view () in let cmd = Helm_registry.get "matita.external_editor" in (* ZACK uncomment to enable interactive ask of external editor command *) (* let cmd = @@ -1200,8 +887,8 @@ class gui () = let script = MatitaScript.current () in let fname = script#filename in let slice mark = - source_buffer#start_iter#get_slice - ~stop:(source_buffer#get_iter_at_mark mark) + source_view#source_buffer#start_iter#get_slice + ~stop:(source_view#source_buffer#get_iter_at_mark mark) in let locked = `MARK script#locked_mark in let string_pos mark = string_of_int (String.length (slice mark)) in @@ -1214,21 +901,21 @@ class gui () = cmd)) in let locked_before = slice locked in - let locked_offset = (source_buffer#get_iter_at_mark locked)#offset in + let locked_offset = (source_view#source_buffer#get_iter_at_mark locked)#offset in ignore (Unix.system cmd); - source_buffer#set_text (HExtlib.input_file fname); - let locked_iter = source_buffer#get_iter (`OFFSET locked_offset) in - source_buffer#move_mark locked locked_iter; - source_buffer#apply_tag script#locked_tag - ~start:source_buffer#start_iter ~stop:locked_iter; + source_view#source_buffer#set_text (HExtlib.input_file fname); + let locked_iter = source_view#source_buffer#get_iter (`OFFSET locked_offset) in + source_view#source_buffer#move_mark locked locked_iter; + source_view#source_buffer#apply_tag script#locked_tag + ~start:source_view#source_buffer#start_iter ~stop:locked_iter; let locked_after = slice locked in let line = ref 0 in let col = ref 0 in try for i = 0 to String.length locked_before - 1 do if locked_before.[i] <> locked_after.[i] then begin - source_buffer#place_cursor - ~where:(source_buffer#get_iter (`LINEBYTE (!line, !col))); + source_view#source_buffer#place_cursor + ~where:(source_view#source_buffer#get_iter (`LINEBYTE (!line, !col))); script#goto `Cursor (); raise Exit end else if locked_before.[i] = '\n' then begin @@ -1241,6 +928,7 @@ class gui () = | Invalid_argument _ -> script#goto `Bottom () method loadScript file = + let source_view = source_view () in let script = MatitaScript.current () in script#reset (); script#assignFileName (Some file); @@ -1261,8 +949,6 @@ class gui () = self#main#saveMenuItem#misc#set_sensitive true method console = console - method sourceView: GSourceView2.source_view = - (source_view: GSourceView2.source_view) method fileSel = fileSel method findRepl = findRepl method main = main @@ -1338,22 +1024,6 @@ class gui () = GtkThread.main (); !text - method private updateFontSize () = - self#sourceView#misc#modify_font_by_name - (sprintf "%s %d" BuildTimeConf.script_font font_size) - - method increaseFontSize () = - font_size <- font_size + 1; - self#updateFontSize () - - method decreaseFontSize () = - font_size <- font_size - 1; - self#updateFontSize () - - method resetFontSize () = - font_size <- default_font_size; - self#updateFontSize () - end let gui () = diff --git a/matita/matita/matitaGuiTypes.mli b/matita/matita/matitaGuiTypes.mli index f10c0201b..8e3932b04 100644 --- a/matita/matita/matitaGuiTypes.mli +++ b/matita/matita/matitaGuiTypes.mli @@ -49,10 +49,8 @@ object method fileSel : MatitaGeneratedGui.fileSelectionWin method main : MatitaGeneratedGui.mainWin method findRepl : MatitaGeneratedGui.findReplWin -(* method toolbar : MatitaGeneratedGui.toolBarWin *) method console: console - method sourceView: GSourceView2.source_view (** {2 Dialogs instantiation} * methods below create a new window on each invocation. You should @@ -63,22 +61,6 @@ object method newConfirmationDialog: unit -> MatitaGeneratedGui.confirmationDialog method newEmptyDialog: unit -> MatitaGeneratedGui.emptyDialog - (** {2 Selections / clipboards handling} *) - - method canCopy: bool - method canCut: bool - method canDelete: bool - method canPaste: bool - method canPastePattern: bool - - method markupSelected: bool - - method copy: unit -> unit - method cut: unit -> unit - method delete: unit -> unit - method paste: unit -> unit - method pastePattern: unit -> unit - (** {2 Utility methods} *) (** ask the used to choose a file with the file chooser @@ -90,11 +72,6 @@ object method askText: ?title:string -> ?msg:string -> unit -> string option method loadScript: string -> unit - - (** {3 Fonts} *) - method increaseFontSize: unit -> unit - method decreaseFontSize: unit -> unit - method resetFontSize: unit -> unit end type paste_kind = [ `Term | `Pattern ] diff --git a/matita/matita/matitaMathView.ml b/matita/matita/matitaMathView.ml index ec536f60e..e00e4fdc5 100644 --- a/matita/matita/matitaMathView.ml +++ b/matita/matita/matitaMathView.ml @@ -632,10 +632,6 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history) self#_load entry; self#_historyAdd entry - (** {2 methods accessing underlying GtkMathView} *) - - method updateFontSize = mathView#set_font_size (MatitaMisc.get_current_font_size ()) - (** {2 methods used by constructor only} *) method win = win @@ -708,10 +704,6 @@ let show_entry ?(reuse=false) t = let refresh_all_browsers () = List.iter (fun b -> b#refresh ~force:false ()) !cicBrowsers -let update_font_sizes () = - List.iter (fun b -> b#updateFontSize) !cicBrowsers; - (cicMathView_instance ())#update_font_size - let get_math_views () = (cicMathView_instance ()) :: (List.map (fun b -> b#mathView) !cicBrowsers) diff --git a/matita/matita/matitaMathView.mli b/matita/matita/matitaMathView.mli index 6cfd83eb3..51bba6b3e 100644 --- a/matita/matita/matitaMathView.mli +++ b/matita/matita/matitaMathView.mli @@ -32,7 +32,6 @@ val sequentsViewer_instance: unit -> MatitaGuiTypes.sequentsViewer (** {2 Global changes} *) val refresh_all_browsers: unit -> unit (** act on all cicBrowsers *) -val update_font_sizes: unit -> unit (** {2 Rendering in a browser} *) diff --git a/matita/matita/matitaMisc.ml b/matita/matita/matitaMisc.ml index 6e733cd1f..fe6fd3557 100644 --- a/matita/matita/matitaMisc.ml +++ b/matita/matita/matitaMisc.ml @@ -191,14 +191,24 @@ let left_button = 1 let middle_button = 2 let right_button = 3 +(* Font size management *) let default_font_size () = Helm_registry.get_opt_default Helm_registry.int ~default:BuildTimeConf.default_font_size "matita.font_size" -let current_font_size = ref ~-1 +let current_font_size = ref (default_font_size ()) +let font_size_observers = ref [];; +let observe_font_size (f: int -> unit) = + f !current_font_size; + font_size_observers := f :: !font_size_observers;; +let observe () = + List.iter (fun f -> f !current_font_size) !font_size_observers;; let get_current_font_size () = !current_font_size -let increase_font_size () = incr current_font_size -let decrease_font_size () = decr current_font_size -let reset_font_size () = current_font_size := default_font_size () +let increase_font_size () = + incr current_font_size; observe () +let decrease_font_size () = + decr current_font_size; observe () +let reset_font_size () = + current_font_size := default_font_size (); observe () let gui_instance = ref None let set_gui (gui : MatitaGuiTypes.gui) = gui_instance := Some gui diff --git a/matita/matita/matitaMisc.mli b/matita/matita/matitaMisc.mli index ed5e5f646..b3bd617b2 100644 --- a/matita/matita/matitaMisc.mli +++ b/matita/matita/matitaMisc.mli @@ -85,10 +85,11 @@ val right_button: int (** {2 Global changes} *) +val observe_font_size: (int -> unit) -> unit val get_current_font_size: unit -> int -val increase_font_size: unit -> unit -val decrease_font_size: unit -> unit -val reset_font_size: unit -> unit +val increase_font_size: unit -> unit +val decrease_font_size: unit -> unit +val reset_font_size: unit -> unit (** CSC: these functions should completely disappear (bad design) *) val set_gui: MatitaGuiTypes.gui -> unit diff --git a/matita/matita/matitaScript.ml b/matita/matita/matitaScript.ml index 75d995f78..a9a86bb80 100644 --- a/matita/matita/matitaScript.ml +++ b/matita/matita/matitaScript.ml @@ -245,12 +245,28 @@ let fresh_script_id = let i = ref 0 in fun () -> incr i; !i -class script ~(source_view: GSourceView2.source_view) - ~ask_confirmation - ~urichooser - () = +(** Selection handling + * Two clipboards are used: "clipboard" and "primary". + * "primary" is used by X, when you hit the middle button mouse is content is + * pasted between applications. In Matita this selection always contain the + * textual version of the selected term. + * "clipboard" is used inside Matita only and support ATM two different targets: + * "TERM" and "PATTERN", in the future other targets like "MATHMLCONTENT" may + * be added + *) +class script ~ask_confirmation ~urichooser () = +let source_view = + GSourceView2.source_view + ~auto_indent:true + ~insert_spaces_instead_of_tabs:true ~tab_width:2 + ~right_margin_position:80 ~show_right_margin:true + ~smart_home_end:`AFTER + ~packing:(MatitaMisc.get_gui ())#main#scriptScrolledWin#add + () in let buffer = source_view#buffer in let source_buffer = source_view#source_buffer in +let similarsymbols_tag_name = "similarsymbolos" in +let similarsymbols_tag = `NAME similarsymbols_tag_name in let initial_statuses current baseuri = let empty_lstatus = new GrafiteDisambiguate.status in (match current with @@ -280,17 +296,25 @@ let default_buri = "cic:/matita/tests" in let default_fname = ".unnamed.ma" in object (self) val mutable include_paths_ = [] + val clipboard = GData.clipboard Gdk.Atom.clipboard + (*val primary = GData.clipboard Gdk.Atom.primary*) + val mutable similarsymbols = [] + val mutable similarsymbols_orig = [] + val similar_memory = Hashtbl.create 97 + val mutable old_used_memory = false val scriptId = fresh_script_id () val guistuff = { - urichooser = urichooser; + urichooser = urichooser source_view; ask_confirmation = ask_confirmation; } val mutable filename_ = (None : string option) method has_name = filename_ <> None + + method source_view = source_view method include_paths = include_paths_ @ @@ -319,10 +343,106 @@ object (self) method filename = match filename_ with None -> default_fname | Some f -> f initializer + MatitaMisc.observe_font_size (fun font_size -> + source_view#misc#modify_font_by_name + (sprintf "%s %d" BuildTimeConf.script_font font_size)); + source_view#misc#grab_focus (); + ignore(source_view#source_buffer#set_language + (Some MatitaGtkMisc.matita_lang)); + ignore(source_view#source_buffer#set_highlight_syntax true); + ignore(source_view#connect#after#paste_clipboard + ~callback:(fun () -> self#clean_dirty_lock)); ignore (GMain.Timeout.add ~ms:300000 ~callback:(fun _ -> self#_saveToBackupFile ();true)); ignore (buffer#connect#modified_changed - (fun _ -> self#set_star buffer#modified)) + (fun _ -> self#set_star buffer#modified)); + (* clean_locked is set to true only "during" a PRIMARY paste + operation (i.e. by clicking with the second mouse button) *) + let clean_locked = ref false in + ignore(source_view#event#connect#button_press + ~callback: + (fun button -> + if GdkEvent.Button.button button = 2 then + clean_locked := true; + false + )); + ignore(source_view#event#connect#button_release + ~callback:(fun button -> clean_locked := false; false)); + ignore(source_view#buffer#connect#after#apply_tag + ~callback:( + fun tag ~start:_ ~stop:_ -> + if !clean_locked && + tag#get_oid = self#locked_tag#get_oid + then + begin + clean_locked := false; + self#clean_dirty_lock; + clean_locked := true + end)); + ignore(source_view#source_buffer#connect#after#insert_text + ~callback:(fun iter str -> + if (MatitaMisc.get_gui ())#main#menuitemAutoAltL#active && (str = " " || str = "\n") then + ignore(self#expand_virtual_if_any iter str))); + 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; + MatitaGtkMisc.connect_menu_item copy self#copy; + MatitaGtkMisc.connect_menu_item cut self#cut; + MatitaGtkMisc.connect_menu_item delete self#delete; + MatitaGtkMisc.connect_menu_item paste self#paste; + MatitaGtkMisc.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); + MatitaGtkMisc.connect_menu_item new_undoMenuItem + (fun () -> self#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); + MatitaGtkMisc.connect_menu_item new_redoMenuItem + (fun () -> self#safe_redo))); + ignore + (source_view#source_buffer#begin_not_undoable_action (); + self#reset (); + self#template (); + source_view#source_buffer#end_not_undoable_action ()) val mutable statements = [] (** executed statements *) @@ -344,6 +464,216 @@ object (self) val locked_tag = buffer#create_tag [`BACKGROUND "lightblue"; `EDITABLE false] val error_tag = buffer#create_tag [`UNDERLINE `SINGLE; `FOREGROUND "red"] + (** 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) + method locked_mark = locked_mark method locked_tag = locked_tag method error_tag = error_tag @@ -702,9 +1032,9 @@ end let _script = ref None -let script ~source_view ~urichooser ~ask_confirmation () +let script ~urichooser ~ask_confirmation () = - let s = new script ~source_view ~ask_confirmation ~urichooser () in + let s = new script ~ask_confirmation ~urichooser () in _script := Some s; s diff --git a/matita/matita/matitaScript.mli b/matita/matita/matitaScript.mli index 02e06d2d1..aab7488a4 100644 --- a/matita/matita/matitaScript.mli +++ b/matita/matita/matitaScript.mli @@ -40,6 +40,14 @@ object method addObserver : (GrafiteTypes.status -> unit) -> unit + (** {2 Unicode handling} *) + method nextSimilarSymbol: unit + + (** {2 Undo/redo} *) + + method safe_undo: unit + method safe_redo: unit + (** {2 History} *) method advance : ?statement:string -> unit -> unit @@ -48,6 +56,22 @@ object method reset: unit -> unit method template: unit -> unit + (** {2 Selections / clipboards handling} *) + + method markupSelected: bool + method canCopy: bool + method canCut: bool + method canDelete: bool + (*CSC: WRONG CODE: we should look in the clipboard instead! *) + method canPaste: bool + method canPastePattern: bool + + method copy: unit -> unit + method cut: unit -> unit + method delete: unit -> unit + method paste: unit -> unit + method pastePattern: unit -> unit + (** {2 Load/save} *) method has_name: bool @@ -74,6 +98,7 @@ object (** misc *) method clean_dirty_lock: unit method set_star: bool -> unit + method source_view: GSourceView2.source_view (* debug *) method dump : unit -> unit @@ -82,8 +107,7 @@ object end val script: - source_view:GSourceView2.source_view -> - urichooser: (NReference.reference list -> NReference.reference list) -> + urichooser: (GSourceView2.source_view -> NReference.reference list -> NReference.reference list) -> ask_confirmation: (title:string -> message:string -> [`YES | `NO | `CANCEL]) -> unit -> -- 2.39.2