From: Stefano Zacchiroli Date: Thu, 28 Jul 2005 14:17:06 +0000 (+0000) Subject: added support for (textual) cut and paste of mathml/boxml markup X-Git-Tag: V_0_7_2~16 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=5c56a926588a63ceac31e6ddd6e3eeb02fadf3a9;p=helm.git added support for (textual) cut and paste of mathml/boxml markup --- diff --git a/helm/matita/.depend b/helm/matita/.depend index 990877d36..b4a1a4c35 100644 --- a/helm/matita/.depend +++ b/helm/matita/.depend @@ -33,13 +33,13 @@ matitaGeneratedGui.cmx: matitaGeneratedGui.cmi matitaGtkMisc.cmo: matitaTypes.cmi matitaGeneratedGui.cmi matitaGtkMisc.cmi matitaGtkMisc.cmx: matitaTypes.cmx matitaGeneratedGui.cmx matitaGtkMisc.cmi matitaGui.cmo: matitamakeLib.cmi matitacleanLib.cmi matitacLib.cmi \ - matitaTypes.cmi matitaScript.cmi matitaMisc.cmi matitaLog.cmi \ - matitaGtkMisc.cmi matitaGeneratedGui.cmi matitaExcPp.cmi \ - buildTimeConf.cmo matitaGui.cmi + matitaTypes.cmi matitaScript.cmi matitaMisc.cmi matitaMathView.cmi \ + matitaLog.cmi matitaGtkMisc.cmi matitaGeneratedGui.cmi matitaExcPp.cmi \ + matitaDisambiguator.cmi buildTimeConf.cmo matitaGui.cmi matitaGui.cmx: matitamakeLib.cmx matitacleanLib.cmx matitacLib.cmx \ - matitaTypes.cmx matitaScript.cmx matitaMisc.cmx matitaLog.cmx \ - matitaGtkMisc.cmx matitaGeneratedGui.cmx matitaExcPp.cmx \ - buildTimeConf.cmx matitaGui.cmi + matitaTypes.cmx matitaScript.cmx matitaMisc.cmx matitaMathView.cmx \ + matitaLog.cmx matitaGtkMisc.cmx matitaGeneratedGui.cmx matitaExcPp.cmx \ + matitaDisambiguator.cmx buildTimeConf.cmx matitaGui.cmi matitaLog.cmo: matitaLog.cmi matitaLog.cmx: matitaLog.cmi matitamakeLib.cmo: matitaMisc.cmi matitaLog.cmi buildTimeConf.cmo \ @@ -49,21 +49,21 @@ matitamakeLib.cmx: matitaMisc.cmx matitaLog.cmx buildTimeConf.cmx \ matitamake.cmo: matitamakeLib.cmi buildTimeConf.cmo matitamake.cmx: matitamakeLib.cmx buildTimeConf.cmx matitaMathView.cmo: matitaTypes.cmi matitaScript.cmi matitaMisc.cmi \ - matitaGui.cmi matitaGtkMisc.cmi matitaExcPp.cmi buildTimeConf.cmo \ - matitaMathView.cmi + matitaLog.cmi matitaGuiTypes.cmi matitaGtkMisc.cmi matitaExcPp.cmi \ + buildTimeConf.cmo matitaMathView.cmi matitaMathView.cmx: matitaTypes.cmx matitaScript.cmx matitaMisc.cmx \ - matitaGui.cmx matitaGtkMisc.cmx matitaExcPp.cmx buildTimeConf.cmx \ - matitaMathView.cmi + matitaLog.cmx matitaGuiTypes.cmi matitaGtkMisc.cmx matitaExcPp.cmx \ + buildTimeConf.cmx matitaMathView.cmi matitaMisc.cmo: matitaTypes.cmi matitaLog.cmi matitaExcPp.cmi \ buildTimeConf.cmo matitaMisc.cmi matitaMisc.cmx: matitaTypes.cmx matitaLog.cmx matitaExcPp.cmx \ buildTimeConf.cmx matitaMisc.cmi matita.cmo: matitamakeLib.cmi matitaTypes.cmi matitaScript.cmi matitaMisc.cmi \ matitaMathView.cmi matitaLog.cmi matitaGui.cmi matitaGtkMisc.cmi \ - matitaEngine.cmi matitaDisambiguator.cmi matitaDb.cmi buildTimeConf.cmo + matitaEngine.cmi matitaDb.cmi buildTimeConf.cmo matita.cmx: matitamakeLib.cmx matitaTypes.cmx matitaScript.cmx matitaMisc.cmx \ matitaMathView.cmx matitaLog.cmx matitaGui.cmx matitaGtkMisc.cmx \ - matitaEngine.cmx matitaDisambiguator.cmx matitaDb.cmx buildTimeConf.cmx + matitaEngine.cmx matitaDb.cmx buildTimeConf.cmx matitaScript.cmo: matitamakeLib.cmi matitacleanLib.cmi matitaTypes.cmi \ matitaSync.cmi matitaMisc.cmi matitaLog.cmi matitaEngine.cmi \ matitaDisambiguator.cmi matitaDb.cmi buildTimeConf.cmo matitaScript.cmi @@ -80,8 +80,8 @@ matitaDisambiguator.cmi: matitaTypes.cmi matitaEngine.cmi: matitaTypes.cmi matitaGtkMisc.cmi: matitaGeneratedGui.cmi matitaGui.cmi: matitaGuiTypes.cmi matitaDisambiguator.cmi -matitaGuiTypes.cmi: matitaLog.cmi matitaGeneratedGui.cmi -matitaMathView.cmi: matitaTypes.cmi +matitaGuiTypes.cmi: matitaTypes.cmi matitaLog.cmi matitaGeneratedGui.cmi +matitaMathView.cmi: matitaTypes.cmi matitaGuiTypes.cmi matitaMisc.cmi: matitaTypes.cmi matitaScript.cmi: matitaTypes.cmi matitaSync.cmi: matitaTypes.cmi diff --git a/helm/matita/matita.ml b/helm/matita/matita.ml index 07def06cd..69bee68a5 100644 --- a/helm/matita/matita.ml +++ b/helm/matita/matita.ml @@ -129,9 +129,9 @@ let _ = List.iter (fun (u,_,_) -> prerr_endline (UriManager.string_of_uri u)) (CicEnvironment.list_obj ())); - addDebugItem "print selected terms" (fun () -> + addDebugItem "print selections" (fun () -> let sequentViewer = MatitaMathView.sequentViewer_instance () in - MatitaLog.debug (sequentViewer#string_of_selected_terms)); + List.iter MatitaLog.debug (sequentViewer#string_of_selections)); addDebugItem "dump getter settings" (fun _ -> prerr_endline (Http_getter_env.env_to_string ())); addDebugItem "getter: getalluris" (fun _ -> diff --git a/helm/matita/matitaGui.ml b/helm/matita/matitaGui.ml index fe0b4a1f9..cf1417229 100644 --- a/helm/matita/matitaGui.ml +++ b/helm/matita/matitaGui.ml @@ -29,7 +29,7 @@ open MatitaGeneratedGui open MatitaGtkMisc open MatitaMisc -let gui_instance = ref None ;; +let gui_instance = ref None class type browserWin = (* this class exists only because GEdit.combo_box_entry is not supported by @@ -129,6 +129,11 @@ class gui () = ~default:BuildTimeConf.default_font_size "matita.font_size" in let source_buffer = source_view#source_buffer in +(* let _ = + source_view#event#connect#selection_clear (fun _ -> + prerr_endline "source_view: selection clear"; + false) + in *) object (self) val mutable chosen_file = None val mutable _ok_not_exists = false @@ -178,8 +183,7 @@ class gui () = ~website:"http://helm.cs.unibo.it" () in - ignore (main#aboutMenuItem#connect#activate - (fun _ -> about_dialog#present ())); + connect_menu_item main#aboutMenuItem about_dialog#present; (* findRepl win *) let show_find_Repl () = findRepl#toplevel#misc#show (); @@ -292,12 +296,12 @@ class gui () = source_view#source_buffer#redo (); source_view#misc#grab_focus () in - ignore(self#main#undoMenuItem#connect#activate ~callback:safe_undo); + connect_menu_item main#undoMenuItem 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); + ~callback:main#undoMenuItem#misc#set_sensitive); + connect_menu_item main#redoMenuItem safe_redo; ignore(source_view#source_buffer#connect#can_redo - ~callback:self#main#redoMenuItem#misc#set_sensitive); + ~callback:main#redoMenuItem#misc#set_sensitive); ignore(source_view#connect#after#populate_popup ~callback:(fun pre_menu -> let menu = new GMenu.menu pre_menu in @@ -316,7 +320,7 @@ class gui () = new_undoMenuItem#misc#set_sensitive (undoMenuItem#misc#get_flag `SENSITIVE); menu#remove (undoMenuItem :> GMenu.menu_item); - ignore(new_undoMenuItem#connect#activate ~callback:safe_undo); + connect_menu_item new_undoMenuItem safe_undo; let new_redoMenuItem = GMenu.image_menu_item ~image:(GMisc.image ~stock:`REDO ()) @@ -326,40 +330,41 @@ class gui () = 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#editMenu#connect#activate - ~callback: - (fun () -> - let something_selected = - (source_buffer#get_iter_at_mark `INSERT)#compare - (source_buffer#get_iter_at_mark `SEL_BOUND) <> 0 - in - self#main#cutMenuItem#misc#set_sensitive something_selected; - self#main#copyMenuItem#misc#set_sensitive something_selected; - self#main#deleteMenuItem#misc#set_sensitive something_selected; - self#main#pasteMenuItem#misc#set_sensitive (clipboard#text <> None) - )); - 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#selectAllMenuItem#connect#activate - ~callback:(fun () -> - source_buffer#move_mark `INSERT source_buffer#start_iter; - source_buffer#move_mark `SEL_BOUND source_buffer#end_iter)); - ignore(self#main#findReplMenuItem#connect#activate - ~callback:show_find_Repl); - ignore (findRepl#findEntry#connect#activate ~callback:find_forward); + connect_menu_item new_redoMenuItem safe_redo)); + let clipboard = GData.clipboard Gdk.Atom.clipboard in + let text_selected () = + (source_buffer#get_iter_at_mark `INSERT)#compare + (source_buffer#get_iter_at_mark `SEL_BOUND) <> 0 + in + let markup_selected () = MatitaMathView.get_selections () <> None in + connect_menu_item main#editMenu (fun () -> + let text_selected = text_selected () in + let markup_selected = markup_selected () in + let something_selected = text_selected || markup_selected in + main#cutMenuItem#misc#set_sensitive text_selected; + main#copyMenuItem#misc#set_sensitive something_selected; + main#deleteMenuItem#misc#set_sensitive text_selected; + main#pasteMenuItem#misc#set_sensitive (clipboard#text <> None)); + connect_menu_item main#cutMenuItem (fun () -> + source_view#buffer#cut_clipboard clipboard); + connect_menu_item main#copyMenuItem (fun () -> + if text_selected () then + source_view#buffer#copy_clipboard clipboard + else if markup_selected () then + match MatitaMathView.get_selections () with + | None + | Some [] -> () + | Some (s :: _) -> clipboard#set_text s); + connect_menu_item main#pasteMenuItem (fun () -> + source_view#buffer#paste_clipboard clipboard; + (MatitaScript.instance ())#clean_dirty_lock); + connect_menu_item main#deleteMenuItem (fun () -> + ignore (source_view#buffer#delete_selection ())); + 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); + connect_menu_item main#findReplMenuItem show_find_Repl; + ignore (findRepl#findEntry#connect#activate find_forward); (* interface lockers *) let lock_world _ = main#buttonsToolbar#misc#set_sensitive false; @@ -435,7 +440,7 @@ class gui () = ignore(develList#toplevel#event#connect#delete (fun _ -> develList#toplevel#misc#hide();true)); let selected_devel = ref None in - connect_menu_item self#main#developmentsMenuItem + connect_menu_item main#developmentsMenuItem (fun () -> refresh_devels_win ();develList#toplevel#misc#show ()); (* add development win *) @@ -531,7 +536,7 @@ class gui () = buf#insert ~iter:(buf#get_iter_at_mark (`NAME "locked")) ("\n" ^ GrafiteAstPp.pp_tactic ast) in - let tbar = self#main in + let tbar = main in connect_button tbar#introsButton (tac (A.Intros (loc, None, []))); connect_button tbar#applyButton (tac_w_term (A.Apply (loc, hole))); connect_button tbar#exactButton (tac_w_term (A.Exact (loc, hole))); @@ -549,19 +554,19 @@ class gui () = connect_button tbar#cutButton (tac_w_term (A.Cut (loc, None, hole))); connect_button tbar#autoButton (tac (A.Auto (loc,None,None,None))); (* ALB *) MatitaGtkMisc.toggle_widget_visibility - ~widget:(self#main#tacticsButtonsHandlebox :> GObj.widget) - ~check:self#main#tacticsBarMenuItem; + ~widget:(main#tacticsButtonsHandlebox :> GObj.widget) + ~check:main#tacticsBarMenuItem; let module Hr = Helm_registry in if not (Hr.get_opt_default Hr.bool ~default:false "matita.tactics_bar") then - self#main#tacticsBarMenuItem#set_active false; + main#tacticsBarMenuItem#set_active false; MatitaGtkMisc.toggle_callback ~callback:(function - | true -> self#main#toplevel#fullscreen () - | false -> self#main#toplevel#unfullscreen ()) - ~check:self#main#fullscreenMenuItem; - self#main#fullscreenMenuItem#set_active false; + | true -> main#toplevel#fullscreen () + | false -> main#toplevel#unfullscreen ()) + ~check:main#fullscreenMenuItem; + main#fullscreenMenuItem#set_active false; (* log *) MatitaLog.set_log_callback self#console#log_callback; GtkSignal.user_handler := @@ -579,7 +584,7 @@ class gui () = let s () = MatitaScript.instance () in let disableSave () = script_fname <- None; - self#main#saveMenuItem#misc#set_sensitive false + main#saveMenuItem#misc#set_sensitive false in let saveAsScript () = let script = s () in @@ -648,7 +653,7 @@ class gui () = let bottom = locker (keep_focus bottom) in let jump = locker (keep_focus jump) in let connect_key sym f = - connect_key self#main#mainWinEventBox#event + connect_key main#mainWinEventBox#event ~modifiers:[`CONTROL] ~stop:true sym f; connect_key self#sourceView#event ~modifiers:[`CONTROL] ~stop:true sym f @@ -685,19 +690,19 @@ class gui () = GMain.Main.quit () with MatitaTypes.Cancel -> ()) end); - connect_button self#main#scriptAdvanceButton advance; - connect_button self#main#scriptRetractButton retract; - connect_button self#main#scriptTopButton top; - connect_button self#main#scriptBottomButton bottom; + connect_button main#scriptAdvanceButton advance; + connect_button main#scriptRetractButton retract; + connect_button main#scriptTopButton top; + connect_button main#scriptBottomButton bottom; connect_key GdkKeysyms._Down advance; connect_key GdkKeysyms._Up retract; connect_key GdkKeysyms._Home top; connect_key GdkKeysyms._End bottom; - connect_button self#main#scriptJumpButton jump; - connect_menu_item self#main#openMenuItem loadScript; - connect_menu_item self#main#saveMenuItem saveScript; - connect_menu_item self#main#saveAsMenuItem saveAsScript; - connect_menu_item self#main#newMenuItem newScript; + connect_button main#scriptJumpButton jump; + connect_menu_item main#openMenuItem loadScript; + connect_menu_item main#saveMenuItem saveScript; + connect_menu_item main#saveAsMenuItem saveAsScript; + connect_menu_item main#newMenuItem newScript; connect_key GdkKeysyms._period (fun () -> source_buffer#insert ~iter:(source_buffer#get_iter_at_mark `INSERT) @@ -711,11 +716,11 @@ class gui () = (* script monospace font stuff *) self#updateFontSize (); (* debug menu *) - self#main#debugMenu#misc#hide (); + main#debugMenu#misc#hide (); (* status bar *) - self#main#hintLowImage#set_file (image_path "matita-bulb-low.png"); - self#main#hintMediumImage#set_file (image_path "matita-bulb-medium.png"); - self#main#hintHighImage#set_file (image_path "matita-bulb-high.png"); + main#hintLowImage#set_file (image_path "matita-bulb-low.png"); + 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 *) @@ -724,8 +729,8 @@ class gui () = let main_w = width * 90 / 100 in let main_h = height * 80 / 100 in let script_w = main_w * 6 / 10 in - self#main#toplevel#resize ~width:main_w ~height:main_h; - self#main#hpaneScriptSequent#set_position script_w; + 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.instance ())#clean_dirty_lock)); @@ -794,9 +799,9 @@ class gui () = script_fname <- Some file; self#main#saveMenuItem#misc#set_sensitive true - method console = console - method sourceView: GSourceView.source_view = (source_view: GSourceView.source_view) + method sourceView: GSourceView.source_view = + (source_view: GSourceView.source_view) method fileSel = fileSel method findRepl = findRepl method main = main @@ -840,7 +845,7 @@ class gui () = keyBindingBoxes method setQuitCallback callback = - ignore (main#quitMenuItem#connect#activate callback); + connect_menu_item main#quitMenuItem callback; ignore (main#toplevel#event#connect#delete (fun _ -> callback ();true)); self#addKeyBinding GdkKeysyms._q callback diff --git a/helm/matita/matitaGuiTypes.mli b/helm/matita/matitaGuiTypes.mli index c4c1007b7..14bfee4f4 100644 --- a/helm/matita/matitaGuiTypes.mli +++ b/helm/matita/matitaGuiTypes.mli @@ -96,7 +96,8 @@ object (** set hyperlink callback. None disable hyperlink handling *) method set_href_callback: (string -> unit) option -> unit - method string_of_selected_terms: string + method string_of_selections: string list + method string_of_selection: string option (* last selected node *) method update_font_size: unit end @@ -121,5 +122,6 @@ object method load: MatitaTypes.mathViewer_entry -> unit (* method loadList: string list -> MatitaTypes.mathViewer_entry -> unit *) method loadInput: string -> unit + method mathView: clickableMathView end diff --git a/helm/matita/matitaMathView.ml b/helm/matita/matitaMathView.ml index 07233700a..f81b2a226 100644 --- a/helm/matita/matitaMathView.ml +++ b/helm/matita/matitaMathView.ml @@ -26,6 +26,7 @@ open Printf open MatitaTypes +open MatitaGtkMisc let add_trailing_slash = let rex = Pcre.regexp "/$" in @@ -60,8 +61,11 @@ 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 () - (* is there any lablgtk2 constant corresponding to the left mouse button??? *) + (* is there any lablgtk2 constant corresponding to the various mouse + * buttons??? *) let left_button = 1 +let middle_button = 2 +let right_button = 3 let near (x1, y1) (x2, y2) = let distance = sqrt (((x2 -. x1) ** 2.) +. ((y2 -. y1) ** 2.)) in @@ -71,58 +75,77 @@ let href_ds = Gdome.domString "href" let xref_ds = Gdome.domString "xref" class clickableMathView obj = - let text_width = 80 in - object (self) - inherit GMathViewAux.multi_selection_math_view obj - - val mutable href_callback: (string -> unit) option = None - method set_href_callback f = href_callback <- f - - val mutable _cic_info = None - method private set_cic_info info = _cic_info <- info - method private cic_info = - match _cic_info with - | Some info -> info - | None -> assert false - - initializer - self#set_font_size !current_font_size; - ignore (self#connect#selection_changed self#choose_selection); - ignore (self#event#connect#button_press self#button_press); - ignore (self#event#connect#button_release self#button_release); -(* ignore (self#connect#click (fun (gdome_elt, _, _, _) -> - match gdome_elt with - | Some elt |+ element is an hyperlink, use href_callback on it +| - when elt#hasAttributeNS ~namespaceURI:DomMisc.xlink_ns ~localName:href -> - (match href_callback with - | None -> () - | Some f -> - let uri = - elt#getAttributeNS ~namespaceURI:DomMisc.xlink_ns ~localName:href - in - f (uri#to_string)) - | Some elt -> ignore (self#action_toggle elt) - | None -> ())) *) - - val mutable button_press_x = -1. - val mutable button_press_y = -1. - val mutable selection_changed = false - - method private button_press gdk_button = - if GdkEvent.Button.button gdk_button = left_button then begin - button_press_x <- GdkEvent.Button.x gdk_button; - button_press_y <- GdkEvent.Button.y gdk_button; - selection_changed <- false - end; - false - - method private button_release gdk_button = - if GdkEvent.Button.button gdk_button = left_button then begin - let button_release_x = GdkEvent.Button.x gdk_button in - let button_release_y = GdkEvent.Button.y gdk_button in - (if near (button_press_x, button_press_y) +let text_width = 80 in +object (self) + inherit GMathViewAux.multi_selection_math_view obj + + val mutable href_callback: (string -> unit) option = None + method set_href_callback f = href_callback <- f + + val mutable _cic_info = None + method private set_cic_info info = _cic_info <- info + method private cic_info = + match _cic_info with + | Some info -> info + | None -> assert false + + initializer + self#set_font_size !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); + ignore (self#event#connect#selection_clear self#selection_clear_cb); + ignore (self#coerce#misc#connect#selection_get self#selection_get_cb); + self#coerce#misc#add_selection_target + ~target:(Gdk.Atom.name Gdk.Atom.string) Gdk.Atom.primary + + val mutable button_press_x = -1. + val mutable button_press_y = -1. + val mutable selection_changed = false +(* val mutable ignore_next_selection_clear = false *) + + method private selection_get_cb ctxt ~info ~time = + (match self#get_selections with + | [] -> () + | node :: _ -> ctxt#return (self#string_of_node node)) + + method private selection_clear_cb sel_event = + self#remove_selections; + false + + method private button_press_cb gdk_button = + let button = GdkEvent.Button.button gdk_button in + if button = left_button then begin + button_press_x <- GdkEvent.Button.x gdk_button; + button_press_y <- GdkEvent.Button.y gdk_button; + selection_changed <- false + end else if button = right_button then + self#popup_contextual_menu (GdkEvent.Button.time gdk_button); + false + + method private popup_contextual_menu time = + match self#string_of_selection with + | None -> () + | Some s -> + let clipboard = GData.clipboard Gdk.Atom.clipboard in + let menu = GMenu.menu () in + let copy_menu_item = + GMenu.image_menu_item + ~label:"_Copy" ~stock:`COPY ~packing:menu#append () + in + connect_menu_item copy_menu_item (fun () -> clipboard#set_text s); + menu#popup ~button:right_button ~time + + method private button_release_cb gdk_button = + let clipboard = GData.clipboard Gdk.Atom.primary in + if GdkEvent.Button.button gdk_button = left_button then begin + let button_release_x = GdkEvent.Button.x gdk_button in + let button_release_y = GdkEvent.Button.y gdk_button in + if selection_changed then + () + else (* selection _not_ changed *) + if near (button_press_x, button_press_y) (button_release_x, button_release_y) - && not selection_changed then let x = int_of_float button_press_x in let y = int_of_float button_press_y in @@ -136,104 +159,86 @@ class clickableMathView obj = (elt#getAttributeNS ~namespaceURI ~localName)#to_string gdk_button else - ignore (self#action_toggle elt))); - end; - false - - method private invoke_href_callback href_value gdk_button = - let button = GdkEvent.Button.button gdk_button in - if button = left_button then - let time = GdkEvent.Button.time gdk_button in - match href_callback with - | None -> () - | Some f -> - (match MatitaMisc.split href_value with - | [ uri ] -> f uri - | uris -> - let menu = GMenu.menu () in - List.iter - (fun uri -> - let menu_item = - GMenu.menu_item ~label:uri ~packing:menu#append () - in - ignore (menu_item#connect#activate (fun () -> f uri))) - uris; - menu#popup ~button ~time) - - method private choose_selection gdome_elt = - let rec aux elt = - if (elt#getAttributeNS ~namespaceURI:DomMisc.helm_ns - ~localName:xref_ds)#to_string <> "" + ignore (self#action_toggle elt)); + end; + false + + method private invoke_href_callback href_value gdk_button = + let button = GdkEvent.Button.button gdk_button in + if button = left_button then + let time = GdkEvent.Button.time gdk_button in + match href_callback with + | None -> () + | Some f -> + (match MatitaMisc.split href_value with + | [ uri ] -> f uri + | uris -> + let menu = GMenu.menu () in + List.iter + (fun uri -> + let menu_item = + GMenu.menu_item ~label:uri ~packing:menu#append () + in + connect_menu_item menu_item (fun () -> f uri)) + uris; + menu#popup ~button ~time) + + method private choose_selection_cb gdome_elt = + let (gui: MatitaGuiTypes.gui) = get_gui () in + let clipboard = GData.clipboard Gdk.Atom.primary in + let rec aux elt = + if (elt#getAttributeNS ~namespaceURI:DomMisc.helm_ns + ~localName:xref_ds)#to_string <> "" (* if elt#hasAttributeNS ~namespaceURI:DomMisc.helm_ns ~localName:xref_ds - && (elt#getAttributeNS ~namespaceURI:DomMisc.helm_ns - ~localName:xref_ds)#to_string <> "" *) - then - self#set_selection (Some elt) - else - try - (match elt#get_parentNode with - | None -> assert false - | Some p -> aux (new Gdome.element_of_node p)) - with GdomeInit.DOMCastException _ -> () -(* debug_print "trying to select above the document root" *) - in - (match gdome_elt with - | Some elt -> aux elt - | None -> self#set_selection None); - selection_changed <- true + && (elt#getAttributeNS ~namespaceURI:DomMisc.helm_ns + ~localName:xref_ds)#to_string <> "" *) + then begin + self#set_selection (Some elt); + ignore (self#coerce#misc#grab_selection Gdk.Atom.primary) + end else + try + (match elt#get_parentNode with + | None -> assert false + | Some p -> aux (new Gdome.element_of_node p)) + with GdomeInit.DOMCastException _ -> () + in + (match gdome_elt with + | Some elt -> aux elt + | None -> self#set_selection None); + selection_changed <- true - method update_font_size = - self#set_font_size !current_font_size + method update_font_size = self#set_font_size !current_font_size - method private get_term_by_id context id = - let ids_to_terms, ids_to_hypotheses = self#cic_info in + method private get_term_by_id context id = + let ids_to_terms, ids_to_hypotheses = self#cic_info in + try + `Term (Hashtbl.find ids_to_terms id) + with Not_found -> try - `Term (Hashtbl.find ids_to_terms id) - with Not_found -> - try - let hyp = Hashtbl.find ids_to_hypotheses id in - let context' = MatitaMisc.list_tl_at hyp context in - `Hyp context' - with Not_found -> assert false - - method string_of_selected_terms = - let get_id (node: Gdome.element) = - let xref_attr = - node#getAttributeNS ~namespaceURI:DomMisc.helm_ns ~localName:xref_ds - in - xref_attr#to_string - in - let script = MatitaScript.instance () in - let metasenv = script#proofMetasenv in - let context = script#proofContext in - let conclusion = script#proofConclusion in - let cic_terms = - List.map - (fun node -> self#get_term_by_id context (get_id node)) - self#get_selections - in -(* TODO: code for patterns - let conclusion = (MatitaScript.instance ())#proofConclusion in - let conclusion_pattern = - ProofEngineHelpers.pattern_of ~term:conclusion cic_terms - in -*) - let dummy_goal = ~-1 in - let cic_sequent = - match cic_terms with - | [] -> assert false - | `Term t :: _ -> - let context' = - ProofEngineHelpers.locate_in_conjecture t - (dummy_goal, context, conclusion) - in - dummy_goal, context', t - | `Hyp context :: _ -> dummy_goal, context, Cic.Rel 1 + let hyp = Hashtbl.find ids_to_hypotheses id in + let context' = MatitaMisc.list_tl_at hyp context in + `Hyp context' + with Not_found -> assert false + + method private string_of_node node = + let get_id (node: Gdome.element) = + let xref_attr = + node#getAttributeNS ~namespaceURI:DomMisc.helm_ns ~localName:xref_ds in + xref_attr#to_string + in + let script = MatitaScript.instance () in + let metasenv = script#proofMetasenv in + let context = script#proofContext in + let conclusion = script#proofConclusion in (* TODO: code for patterns - (* TODO context shouldn't be empty *) - let cic_sequent = ~-1, [], conclusion_pattern in + let conclusion = (MatitaScript.instance ())#proofConclusion in + let conclusion_pattern = + ProofEngineHelpers.pattern_of ~term:conclusion cic_terms + in *) + let dummy_goal = ~-1 in + let string_of_cic_sequent cic_sequent = let acic_sequent, _, _, ids_to_inner_sorts, _ = Cic2acic.asequent_of_sequent metasenv cic_sequent in @@ -244,8 +249,29 @@ class clickableMathView obj = let pped_ast = CicNotationRew.pp_ast ast in let markup = CicNotationPres.render ids_to_uris pped_ast in BoxPp.render_to_string text_width markup + in + let term = self#get_term_by_id context (get_id node) in + let cic_sequent = + match term with + | `Term t -> + let context' = + ProofEngineHelpers.locate_in_conjecture t + (dummy_goal, context, conclusion) + in + dummy_goal, context', t + | `Hyp context -> dummy_goal, context, Cic.Rel 1 + in + string_of_cic_sequent cic_sequent - end + method string_of_selections = + List.map self#string_of_node (List.rev self#get_selections) + + method string_of_selection = + match self#get_selections with + | [] -> None + | node :: _ -> Some (self#string_of_node node) + +end let clickableMathView ?hadjustment ?vadjustment ?font_size ?log_verbosity = GtkBase.Widget.size_params @@ -266,7 +292,7 @@ object (self) in self#set_cic_info (Some (ids_to_terms, ids_to_hypotheses)); let name = "sequent_viewer.xml" in - prerr_endline ("load_sequent: dumping MathML to ./" ^ name); + MatitaLog.debug ("load_sequent: dumping MathML to ./" ^ name); ignore (DomMisc.domImpl#saveDocumentToFile ~name ~doc:mathml ()); self#load_root ~root:mathml#get_documentElement end @@ -404,13 +430,6 @@ type term_source = | `String of string ] -class type cicBrowser = -object - method load: MatitaTypes.mathViewer_entry -> unit - (* method loadList: string list -> MatitaTypes.mathViewer_entry-> unit *) - method loadInput: string -> unit -end - let reloadable = function | `About `Current_proof | `Dir _ -> @@ -528,6 +547,8 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history) val mutable lastDir = "" (* last loaded "directory" *) + method mathView = (mathView :> MatitaGuiTypes.clickableMathView) + method private _getSelectedUri () = match model#easy_selection () with | [sel] when is_uri sel -> sel (* absolute URI selected *) @@ -661,7 +682,7 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history) mathView#thaw | _ -> let name = "cic_browser.xml" in - prerr_endline ("cic_browser: dumping MathML to ./" ^ name); + MatitaLog.debug ("cic_browser: dumping MathML to ./" ^ name); ignore (DomMisc.domImpl#saveDocumentToFile ~name ~doc:mathml ()); mathView#load_root ~root:mathml#get_documentElement; current_mathml <- Some mathml); @@ -745,7 +766,7 @@ let cicBrowser () = GdkKeysyms._W (fun () -> win#toplevel#destroy ()); *) cicBrowsers := browser :: !cicBrowsers; - (browser :> cicBrowser) + (browser :> MatitaGuiTypes.cicBrowser) in let history = new MatitaMisc.browser_history size (`About `Blank) in aux history @@ -765,7 +786,7 @@ let mathViewer () = if reuse then (match !cicBrowsers with | [] -> cicBrowser () - | b :: _ -> (b :> cicBrowser)) + | b :: _ -> (b :> MatitaGuiTypes.cicBrowser)) else (cicBrowser ()) @@ -781,3 +802,24 @@ let update_font_sizes () = List.iter (fun b -> b#updateFontSize) !cicBrowsers; (sequentViewer_instance ())#update_font_size +let get_math_views () = + ((sequentViewer_instance ()) :> MatitaGuiTypes.clickableMathView) + :: (List.map (fun b -> b#mathView) !cicBrowsers) + +let get_selections () = + if (MatitaScript.instance ())#onGoingProof () then + let rec aux = + function + | [] -> None + | mv :: tl -> + (match mv#string_of_selections with + | [] -> aux tl + | sels -> Some sels) + in + aux (get_math_views ()) + else + None + +let reset_selections () = + List.iter (fun mv -> mv#remove_selections) (get_math_views ()) + diff --git a/helm/matita/matitaMathView.mli b/helm/matita/matitaMathView.mli index bee32796e..f4a724160 100644 --- a/helm/matita/matitaMathView.mli +++ b/helm/matita/matitaMathView.mli @@ -50,7 +50,9 @@ val sequentsViewer: val cicBrowser: unit -> MatitaGuiTypes.cicBrowser -(** {2 Mathview wide functions} *) +(** {2 MathView wide functions} *) +(* TODO ZACK consider exporting here a single function which return a list of + * MatitaGuiTypes.clickableMathView and act on them externally ... *) val increase_font_size: unit -> unit val decrease_font_size: unit -> unit @@ -59,6 +61,14 @@ val reset_font_size: unit -> unit val refresh_all_browsers: unit -> unit (** act on all cicBrowsers *) val update_font_sizes: unit -> unit + (** {3 selection handling} *) + + (* @return the selections of a (unspecified) math viewer *) +val get_selections: unit -> string list option + + (* remove the selections of all math viewers *) +val reset_selections: unit -> unit + (** {2 Singleton instances} *) val sequentViewer_instance: unit -> MatitaGuiTypes.sequentViewer