| 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.AVariable (_, _, None, ty, _, _) ->
+ return_father id (mk_ids (ty::inner_types))
| Cic.AInductiveDefinition _ ->
assert false (* TODO *)
+ (** @return string content of a dom node having a single text child node, e.g.
+ * <m:mi xlink:href="...">bool</m:mi> *)
+let string_of_dom_node node =
+ match node#get_firstChild with
+ | None -> ""
+ | Some node ->
+ (try
+ let text = new Gdome.text_of_node node in
+ text#get_data#to_string
+ with GdomeInit.DOMCastException _ -> "")
+
class clickableMathView obj =
let text_width = 80 in
object (self)
method private choose_selection_cb gdome_elt =
let (gui: MatitaGuiTypes.gui) = get_gui () in
let clipboard = GData.clipboard Gdk.Atom.primary in
+ let set_selection elt =
+ 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)
+ 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
+ then
+ set_selection elt
+ else
try
(match elt#get_parentNode with
| None -> assert false
with GdomeInit.DOMCastException _ -> ()
in
(match gdome_elt with
+ | Some elt when (elt#getAttributeNS ~namespaceURI:DomMisc.xlink_ns
+ ~localName:href_ds)#to_string <> "" ->
+ set_selection elt
| Some elt -> aux elt
| None -> self#set_selection None);
selection_changed <- true
(try Hashtbl.find ids_to_terms id with Not_found -> assert false)
method private string_of_node node =
+ if node#hasAttributeNS ~namespaceURI:DomMisc.xlink_ns ~localName:href_ds
+ then string_of_dom_node node
+ else self#string_of_id_node node
+
+ method private string_of_id_node node =
let get_id (node: Gdome.element) =
let xref_attr =
node#getAttributeNS ~namespaceURI:DomMisc.helm_ns ~localName:xref_ds
w#remove cicMathView#coerce;
scrolledWin <- None
| None -> ());
- for i = 0 to pages do notebook#remove_page 0 done;
+ (match switch_page_callback with
+ | Some id ->
+ GtkSignal.disconnect notebook#as_widget id;
+ switch_page_callback <- None
+ | None -> ());
+ for i = 0 to pages do notebook#remove_page 0 done;
notebook#set_show_tabs true;
pages <- 0;
page2goal <- [];
goal2page <- [];
goal2win <- [];
- _metasenv <- [];
+ _metasenv <- [];
self#script#setGoal ~-1;
- (match switch_page_callback with
- | Some id ->
- GtkSignal.disconnect notebook#as_widget id;
- switch_page_callback <- None
- | None -> ())
method load_sequents (status: ProofEngineTypes.status) =
let ((_, metasenv, _, _), goal) = status in