| SelTerm of Cic.term * string option (* term, parent hypothesis (if any) *)
| SelHyp of string * Cic.context (* hypothesis, context *)
+let hrefs_of_elt elt =
+ let localName = href_ds in
+ if elt#hasAttributeNS ~namespaceURI:xlink_ns ~localName then
+ let text =
+ (elt#getAttributeNS ~namespaceURI:xlink_ns ~localName)#to_string in
+ Some (HExtlib.split text)
+ else
+ None
+
class clickableMathView obj =
let text_width = 80 in
object (self)
method private set_cic_info info = _cic_info <- info
method private cic_info = _cic_info
+ val normal_cursor = Gdk.Cursor.create `LEFT_PTR
+ val href_cursor = Gdk.Cursor.create `HAND1
+
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#connect#element_over self#element_over_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
+ val mutable href_statusbar_msg:
+ (GMisc.statusbar_context * Gtk.statusbar_message) option = None
+ (* <statusbar ctxt, statusbar msg> *)
method private selection_get_cb ctxt ~info ~time =
let text =
self#popup_contextual_menu (GdkEvent.Button.time gdk_button);
false
+ method private element_over_cb (elt_opt, _, _, _) =
+ let win () = self#misc#window in
+ let leave_href () =
+ Gdk.Window.set_cursor (win ()) normal_cursor;
+ HExtlib.iter_option (fun (ctxt, msg) -> ctxt#remove msg)
+ href_statusbar_msg
+ in
+ match elt_opt with
+ | Some elt ->
+ (match hrefs_of_elt elt with
+ | Some ((_ :: _) as hrefs) ->
+ Gdk.Window.set_cursor (win ()) href_cursor;
+ let msg_text = (* now create statusbar msg and store it *)
+ match hrefs with
+ | [ href ] -> sprintf "Hyperlink to %s" href
+ | _ -> sprintf "Hyperlinks to: %s" (String.concat ", " hrefs) in
+ let ctxt = (get_gui ())#main#statusBar#new_context ~name:"href" in
+ let msg = ctxt#push msg_text in
+ href_statusbar_msg <- Some (ctxt, msg)
+ | _ -> leave_href ())
+ | None -> leave_href ()
+
(** @return a pattern structure which contains pretty printed terms *)
method private tactic_text_pattern_of_selection =
match self#get_selections with
(match self#get_element_at x y with
| None -> ()
| Some elt ->
- let localName = href_ds in
- if elt#hasAttributeNS ~namespaceURI:xlink_ns ~localName then
- self#invoke_href_callback
- (elt#getAttributeNS ~namespaceURI:xlink_ns
- ~localName)#to_string
- gdk_button
- else
- ignore (self#action_toggle elt));
+ (match hrefs_of_elt elt with
+ | Some hrefs -> self#invoke_href_callback hrefs gdk_button
+ | None -> ignore (self#action_toggle elt)))
end;
false
- method private invoke_href_callback href_value gdk_button =
+ method private invoke_href_callback hrefs 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 HExtlib.split href_value with
+ (match hrefs with
| [ uri ] -> f uri
| uris ->
let menu = GMenu.menu () in
object (self)
inherit scriptAccessor
+ method cicMathView = cicMathView (** clickableMathView accessor *)
+
val mutable pages = 0
val mutable switch_page_callback = None
val mutable page2goal = [] (* associative list: page no -> goal no *)