+let cicBrowsers = ref []
+let gui_instance = ref None
+let set_gui gui = gui_instance := Some gui
+let get_gui () =
+ match !gui_instance with
+ | None -> assert false
+ | Some gui -> gui
+
+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 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 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
+ (distance < 4.)
+
+let href_ds = Gdome.domString "href"
+let xref_ds = Gdome.domString "xref"
+
+(* ids_to_terms should not be passed here, is just for debugging *)
+let find_root_id annobj id ids_to_father_ids ids_to_terms ids_to_inner_types =
+ let find_parent id ids =
+ let rec aux id =
+(* (prerr_endline (sprintf "id %s = %s" id
+ (try
+ CicPp.ppterm (Hashtbl.find ids_to_terms id)
+ with Not_found -> "NONE"))); *)
+ if List.mem id ids then Some id
+ else
+ (match
+ (try Hashtbl.find ids_to_father_ids id with Not_found -> None)
+ with
+ | None -> None
+ | Some id' -> aux id')
+ in
+ aux id
+ in
+ let return_father id ids =
+ match find_parent id ids with
+ | None -> assert false
+ | Some parent_id -> parent_id
+ in
+ let mk_ids terms = List.map CicUtil.id_of_annterm terms in
+ let inner_types =
+ Hashtbl.fold
+ (fun _ types acc ->
+ match types.Cic2acic.annexpected with
+ None -> types.Cic2acic.annsynthesized :: acc
+ | Some ty -> ty :: types.Cic2acic.annsynthesized :: acc
+ ) ids_to_inner_types [] in
+ match annobj with
+ | Cic.AConstant (_, _, _, Some bo, ty, _, _)
+ | Cic.AVariable (_, _, Some bo, ty, _, _)
+ | Cic.ACurrentProof (_, _, _, _, bo, ty, _, _) ->
+ return_father id (mk_ids (ty :: bo :: inner_types))
+ | Cic.AConstant (_, _, _, None, ty, _, _)
+ | Cic.AVariable (_, _, None, ty, _, _) -> return_father id (mk_ids (ty::inner_types))
+ | Cic.AInductiveDefinition _ ->
+ assert false (* TODO *)
+
+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 = _cic_info
+
+ 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)
+
+ val mutable button_press_x = -1.
+ val mutable button_press_y = -1.
+ val mutable selection_changed = 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)
+ then
+ let x = int_of_float button_press_x in
+ let y = int_of_float button_press_y in
+ (match self#get_element_at x y with
+ | None -> ()
+ | Some elt ->
+ let namespaceURI = DomMisc.xlink_ns in
+ let localName = href_ds in
+ if elt#hasAttributeNS ~namespaceURI ~localName then
+ self#invoke_href_callback
+ (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
+ 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 begin
+ self#set_selection (Some elt);
+ self#coerce#misc#add_selection_target
+ ~target:(Gdk.Atom.name Gdk.Atom.string) Gdk.Atom.primary;
+ 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