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 \
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
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
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 _ ->
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
~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
~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 ();
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
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 ())
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;
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 *)
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)));
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 :=
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
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
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)
(* 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 *)
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));
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
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
(** 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
method load: MatitaTypes.mathViewer_entry -> unit
(* method loadList: string list -> MatitaTypes.mathViewer_entry -> unit *)
method loadInput: string -> unit
+ method mathView: clickableMathView
end
open Printf
open MatitaTypes
+open MatitaGtkMisc
let add_trailing_slash =
let rex = Pcre.regexp "/$" in
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
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
(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
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
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
| `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 _ ->
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 *)
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);
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
if reuse then
(match !cicBrowsers with
| [] -> cicBrowser ()
- | b :: _ -> (b :> cicBrowser))
+ | b :: _ -> (b :> MatitaGuiTypes.cicBrowser))
else
(cicBrowser ())
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 ())
+
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
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
projects / helm.git / commitdiff