let distance = sqrt (((x2 -. x1) ** 2.) +. ((y2 -. y1) ** 2.)) in
(distance < 4.)
+let mathml_ns = Gdome.domString "http://www.w3.org/1998/Math/MathML"
let xlink_ns = Gdome.domString "http://www.w3.org/1999/xlink"
let helm_ns = Gdome.domString "http://www.cs.unibo.it/helm"
let href_ds = Gdome.domString "href"
+let maction_ds = Gdome.domString "maction"
let xref_ds = Gdome.domString "xref"
let domImpl = Gdome.domImplementation ()
else
None
+let rec has_maction (elt :Gdome.element) =
+ (* fix this comparison *)
+ if elt#get_tagName#to_string = "m:maction" ||
+ elt#get_tagName#to_string = "b:action" then
+ true
+ else
+ match elt#get_parentNode with
+ | Some node when node#get_nodeType = GdomeNodeTypeT.ELEMENT_NODE ->
+ has_maction (new Gdome.element_of_node node)
+ | _ -> false
+;;
+
class clickableMathView obj =
let text_width = 80 in
object (self)
method private cic_info = _cic_info
val normal_cursor = Gdk.Cursor.create `LEFT_PTR
- val href_cursor = Gdk.Cursor.create `HAND1
+ val href_cursor = Gdk.Cursor.create `HAND2
+ val maction_cursor = Gdk.Cursor.create `QUESTION_ARROW
initializer
self#set_font_size !current_font_size;
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);
+ self#popup_contextual_menu
+ (self#get_element_at
+ (int_of_float (GdkEvent.Button.x gdk_button))
+ (int_of_float (GdkEvent.Button.y gdk_button)))
+ (GdkEvent.Button.time gdk_button);
false
method private element_over_cb (elt_opt, _, _, _) =
in
match elt_opt with
| Some elt ->
+ if has_maction elt then
+ Gdk.Window.set_cursor (win ()) maction_cursor
+ else
(match hrefs_of_elt elt with
| Some ((_ :: _) as hrefs) ->
Gdk.Window.set_cursor (win ()) href_cursor;
| [] -> assert false (* this method is invoked only if there's a sel. *)
| node :: _ -> self#tactic_text_pattern_of_node node
- method private popup_contextual_menu time =
+ method private popup_contextual_menu element time =
let menu = GMenu.menu () in
let add_menu_item ?(menu = menu) ?stock ?label () =
GMenu.image_menu_item ?stock ?label ~packing:menu#append () in
let check = add_menu_item ~label:"Check" () in
let reductions_menu_item = GMenu.menu_item ~label:"βδιζ-reduce" () in
let tactics_menu_item = GMenu.menu_item ~label:"Apply tactic" () in
+ let hyperlinks_menu_item = GMenu.menu_item ~label:"Hyperlinks" () in
menu#append reductions_menu_item;
menu#append tactics_menu_item;
+ menu#append hyperlinks_menu_item;
let reductions = GMenu.menu () in
let tactics = GMenu.menu () in
+ let hyperlinks = GMenu.menu () in
reductions_menu_item#set_submenu reductions;
tactics_menu_item#set_submenu tactics;
+ hyperlinks_menu_item#set_submenu hyperlinks;
let normalize = add_menu_item ~menu:reductions ~label:"Normalize" () in
let simplify = add_menu_item ~menu:reductions ~label:"Simplify" () in
let whd = add_menu_item ~menu:reductions ~label:"Weak head" () in
+ (match element with
+ | None -> hyperlinks_menu_item#misc#set_sensitive false
+ | Some elt ->
+ match hrefs_of_elt elt, href_callback with
+ | Some l, Some f ->
+ List.iter
+ (fun h ->
+ let item = add_menu_item ~menu:hyperlinks ~label:h () in
+ connect_menu_item item (fun () -> f h)) l
+ | _ -> hyperlinks_menu_item#misc#set_sensitive false);
menu#append (GMenu.separator_item ());
let copy = add_menu_item ~stock:`COPY () in
let gui = get_gui () in
(match self#get_element_at x y with
| None -> ()
| Some elt ->
+ if has_maction elt then ignore(self#action_toggle elt) else
(match hrefs_of_elt elt with
| Some hrefs -> self#invoke_href_callback hrefs gdk_button
- | None -> ignore (self#action_toggle elt)))
+ | None -> ()))
end;
false
self#_showGviz
method private tex () =
- let text = String.concat "\n"
- (List.map (fun (k,vs) ->
- let vs =
- List.sort (fun a b -> String.length a - String.length b) vs
- in
- let vs =
- if List.length vs < 4 then vs else
- let vs, _ = HExtlib.split_nth 4 vs in vs
- in
- k ^ "\t" ^ String.concat ", " vs)
- (Utf8Macro.pp_table ()))
- in
- self#_loadText text
+ let b = Buffer.create 1000 in
+ Printf.bprintf b "UTF-8 equivalence classes (rotate with ALT-L):\n\n";
+ List.iter
+ (fun l ->
+ List.iter (fun sym ->
+ Printf.bprintf b " %s" (Glib.Utf8.from_unichar sym)
+ ) l;
+ Printf.bprintf b "\n";
+ )
+ (List.sort
+ (fun l1 l2 -> compare (List.hd l1) (List.hd l2))
+ (Virtuals.get_all_eqclass ()));
+ Printf.bprintf b "\n\nVirtual keys (trigger with ALT-L):\n\n";
+ List.iter
+ (fun tag, items ->
+ Printf.bprintf b " %s:\n" tag;
+ List.iter
+ (fun names, symbol ->
+ Printf.bprintf b " \t%s\t%s\n"
+ (Glib.Utf8.from_unichar symbol)
+ (String.concat ", " names))
+ (List.sort
+ (fun (_,a) (_,b) -> compare a b)
+ items);
+ Printf.bprintf b "\n")
+ (List.sort
+ (fun (a,_) (b,_) -> compare a b)
+ (Virtuals.get_all_virtuals ()));
+ self#_loadText (Buffer.contents b)
method private _loadText text =
searchText#source_buffer#set_text text;