LABLGTK_DIR = /usr/lib/ocaml/lablgtk
LABLGTK_MATHVIEW_DIR = /usr/lib/ocaml/lablgtk/mathview
+MINIDOM_DIR = /usr/lib/ocaml/lablgtk/mathview/minidom
PXP_DIR = /usr/lib/ocaml/site-lib/pxp
NETSTRING_DIR = /usr/lib/ocaml/site-lib/netstring
-OCAMLC = ocamlc -I $(LABLGTK_DIR) -I $(LABLGTK_MATHVIEW_DIR) -I $(PXP_DIR) -I $(NETSTRING_DIR) -I mlmathview
-OCAMLOPT = ocamlopt -I $(LABLGTK_DIR) -I $(LABLGTK_MATHVIEW_DIR) -I mlgtk_devel -I $(PXP_DIR) -I $(NETSTRING_DIR) -I mlmathview
+OCAMLC = ocamlc -I $(LABLGTK_DIR) -I $(LABLGTK_MATHVIEW_DIR) -I $(PXP_DIR) -I $(NETSTRING_DIR) -I $(MINIDOM_DIR) -I mlmathview
+OCAMLOPT = ocamlopt -I $(LABLGTK_DIR) -I $(LABLGTK_MATHVIEW_DIR) -I mlgtk_devel -I $(PXP_DIR) -I $(NETSTRING_DIR) -I $(MINIDOM_DIR) -I mlmathview
OCAMLDEP = ocamldep
all: experiment reduction fix_params mmlinterface
$(OCAMLC) -custom -o mmlinterface str.cma unix.cma $(PXPLIBS) dbm.cma \
lablgtk.cma gtkInit.cmo \
$(LABLGTK_MATHVIEW_DIR)/lablgtkmathview.cma \
+ $(MINIDOM_DIR)/minidom.cmo \
$(MMLINTERFACEOBJS) \
-cclib "-lstr -L/usr/lib -L/usr/X11R6/lib -lgtk -lgdk \
-rdynamic -lgmodule -lglib -ldl -lXi -lXext -lX11 -lm \
-lunix -L/usr/local/lib/gtkmathview -lgtkmathview \
- $(LABLGTK_MATHVIEW_DIR)/ml_gtk_mathview.o" \
+ $(LABLGTK_MATHVIEW_DIR)/ml_gtk_mathview.o \
+ $(MINIDOM_DIR)/ml_minidom.o" \
-cclib -lmldbm -cclib -lndbm
mmlinterface.opt: $(MMLINTERFACEOPTOBJS)
$(OCAMLOPT) -o mmlinterface.opt str.cmxa $(PXPLIBSOPT) unix.cmxa \
dbm.cmxa lablgtk.cmxa gtkInit.cmx \
$(LABLGTK_MATHVIEW_DIR)/lablgtkmathview.cmxa \
+ $(MINIDOM_DIR)/minidom.cmx \
$(MMLINTERFACEOPTOBJS) \
-cclib "-lstr -L/usr/lib -L/usr/X11R6/lib -lgtk -lgdk \
-rdynamic -lgmodule -lglib -ldl -lXi -lXext -lX11 -lm \
-lunix -L/usr/local/lib/gtkmathview -lgtkmathview \
- $(LABLGTK_MATHVIEW_DIR)/ml_gtk_mathview.o" \
+ $(LABLGTK_MATHVIEW_DIR)/ml_gtk_mathview.o \
+ $(MINIDOM_DIR)/ml_minidom.o" \
-cclib -lmldbm -cclib -lndbm
fix_params: $(FIX_PARAMSOBJS)
;;
(* called when an hyperlink is clicked *)
-let jump rendering_window s =
- let uri = UriManager.uri_of_string s in
- rendering_window#show () ;
- rendering_window#prevb#misc#set_sensitive true ;
- rendering_window#nextb#misc#set_sensitive false ;
- visited_uris := uri::!visited_uris ;
- to_visit_uris := [] ;
- annotated_obj := None ;
- update_output rendering_window uri
+let jump rendering_window node =
+ let module M = Minidom in
+ let s =
+ match M.node_get_attribute node (M.mDOMString_of_string "href") with
+ None -> assert false
+ | Some s -> M.string_of_mDOMString s
+ in
+ let uri = UriManager.uri_of_string s in
+ rendering_window#show () ;
+ rendering_window#prevb#misc#set_sensitive true ;
+ rendering_window#nextb#misc#set_sensitive false ;
+ visited_uris := uri::!visited_uris ;
+ to_visit_uris := [] ;
+ annotated_obj := None ;
+ update_output rendering_window uri
+;;
+
+let choose_selection rendering_window node =
+ let module M = Minidom in
+ let rec aux ~first_time node =
+ match M.node_get_attribute node (M.mDOMString_of_string "xref") with
+ None ->
+ let parent =
+ match M.node_get_parent node with
+ None -> assert false
+ | Some parent -> parent
+ in
+ aux ~first_time:false parent
+ | Some s ->
+ if not first_time then
+ rendering_window#output#set_selection (Some node)
+ in
+ match node with
+ None -> () (* No element selected *)
+ | Some node -> aux ~first_time:true node
;;
let changefont rendering_window () =
;;
let annotateb_pressed rendering_window annotation_window () =
- let xpath = (rendering_window#output#get_selection : string option) in
- match xpath with
- None -> (rendering_window#errors : GEdit.text)#insert "\nNo selection!\n"
- | Some xpath ->
- try
- let annobj = get_annotated_obj ()
- (* next "cast" can't got rid of, but I don't know why *)
- and annotation = (annotation_window#annotation : GEdit.text) in
- ann := CicXPath.get_annotation annobj xpath ;
- CicAnnotationHinter.create_hints annotation_window annobj xpath ;
- annotation#delete_text 0 annotation#length ;
- begin
- match !(!ann) with
- None ->
- annotation#misc#set_sensitive false ;
- annotation_window#radio_none#set_active true ;
- radio_some_status := false
- | Some ann' ->
- annotation#insert ann' ;
- annotation#misc#set_sensitive true ;
- annotation_window#radio_some#set_active true ;
- radio_some_status := true
- end ;
- GMain.Grab.add (annotation_window#window_to_annotate#coerce) ;
- annotation_window#show () ;
- with
- e ->
+ let module M = Minidom in
+ match rendering_window#output#get_selection with
+ None -> (rendering_window#errors : GEdit.text)#insert "\nNo selection!\n"
+ | Some node ->
+ let xpath =
+ match M.node_get_attribute node (M.mDOMString_of_string "xref") with
+ None -> assert false
+ | Some xpath -> M.string_of_mDOMString xpath
+ in
+ try
+ let annobj = get_annotated_obj ()
(* next "cast" can't got rid of, but I don't know why *)
- let errors = (rendering_window#errors : GEdit.text) in
- errors#insert ("\n" ^ Printexc.to_string e ^ "\n")
+ and annotation = (annotation_window#annotation : GEdit.text) in
+ ann := CicXPath.get_annotation annobj xpath ;
+ CicAnnotationHinter.create_hints annotation_window annobj xpath ;
+ annotation#delete_text 0 annotation#length ;
+ begin
+ match !(!ann) with
+ None ->
+ annotation#misc#set_sensitive false ;
+ annotation_window#radio_none#set_active true ;
+ radio_some_status := false
+ | Some ann' ->
+ annotation#insert ann' ;
+ annotation#misc#set_sensitive true ;
+ annotation_window#radio_some#set_active true ;
+ radio_some_status := true
+ end ;
+ GMain.Grab.add (annotation_window#window_to_annotate#coerce) ;
+ annotation_window#show () ;
+ with
+ e ->
+ (* next "cast" can't got rid of, but I don't know why *)
+ let errors = (rendering_window#errors : GEdit.text) in
+ errors#insert ("\n" ^ Printexc.to_string e ^ "\n")
;;
(* called when the annotation is confirmed *)
(* signal handlers here *)
ignore(output#connect#jump (jump self)) ;
+ ignore(output#connect#selection_changed (choose_selection self)) ;
ignore(nextb#connect#clicked (next self)) ;
ignore(prevb#connect#clicked (prev self)) ;
ignore(checkb#connect#clicked (check self)) ;
(* signal handlers here *)
ignore(output#connect#jump (jump rendering_window)) ;
+ ignore(output#connect#selection_changed (choose_selection self)) ;
ignore(nextb#connect#clicked (theory_next self)) ;
ignore(prevb#connect#clicked (theory_prev self)) ;
ignore(checkb#connect#clicked (theory_check self)) ;
projects / helm.git / commitdiff