+ method load_root ~root:(hyperlinks,text) =
+ self#buffer#set_text text;
+ let all_tag = self#buffer#create_tag [] in
+ self#buffer#apply_tag all_tag ~start:(self#buffer#get_iter `START)
+ ~stop:(self#buffer#get_iter `END);
+ ignore(all_tag#connect#event
+ ~callback:(fun ~origin:_ event _pos ->
+ match GdkEvent.get_type event with
+ | `MOTION_NOTIFY ->
+ Gdk.Window.set_cursor
+ (match self#get_window `TEXT with None -> assert false | Some x -> x)
+ (Gdk.Cursor.create `ARROW);
+ HExtlib.iter_option (fun (ctxt, msg) -> ctxt#remove msg)
+ href_statusbar_msg;
+ false
+ | _ -> false));
+ let hyperlink_tag = self#buffer#create_tag [] in
+ ignore(hyperlink_tag#connect#event
+ ~callback:(fun ~origin:_ event pos ->
+ let offset = (new GText.iter pos)#offset in
+ let _,_,href =
+ try
+ List.find
+ (fun (start,stop,_href) -> start <= offset && offset <= stop
+ ) hyperlinks
+ with
+ Not_found -> assert false
+ in
+ match GdkEvent.get_type event with
+ `BUTTON_PRESS ->
+ (match href_callback with
+ None -> ()
+ | Some f -> f href);
+ true
+ | `MOTION_NOTIFY ->
+ Gdk.Window.set_cursor
+ (match self#get_window `TEXT with None -> assert false | Some x -> x)
+ (Gdk.Cursor.create `HAND1);
+ let ctxt = (MatitaMisc.get_gui ())#main#statusBar#new_context ~name:"href" in
+ let msg = ctxt#push href in
+ href_statusbar_msg <- Some (ctxt, msg);
+ false
+ | _ -> false));
+ List.iter
+ ( fun (start,stop,(_href : string)) ->
+ self#buffer#apply_tag hyperlink_tag
+ ~start:(self#buffer#get_iter_at_char start)
+ ~stop:(self#buffer#get_iter_at_char (stop+1));
+ ) hyperlinks
+
+