From e6a36a24f7c27739067073172a387b85cd0a6c5c Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Wed, 8 Nov 2000 18:51:25 +0000 Subject: [PATCH] Porting to lablgtk_gtkmathview-0.2.0 completed --- helm/interface/Makefile | 13 ++-- helm/interface/mkindex.sh | 2 +- helm/interface/mmlinterface.ml | 109 +++++++++++++++++++++------------ helm/interface/servers.txt | 1 + 4 files changed, 82 insertions(+), 43 deletions(-) diff --git a/helm/interface/Makefile b/helm/interface/Makefile index 981454830..8bb54e9ad 100644 --- a/helm/interface/Makefile +++ b/helm/interface/Makefile @@ -1,9 +1,10 @@ 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 @@ -106,22 +107,26 @@ mmlinterface: $(MMLINTERFACEOBJS) $(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) diff --git a/helm/interface/mkindex.sh b/helm/interface/mkindex.sh index b47864fae..75156a0c4 100755 --- a/helm/interface/mkindex.sh +++ b/helm/interface/mkindex.sh @@ -1,3 +1,3 @@ #!/bin/bash -echo `find . -name "*.xml"` | /really_very_local/helm/PARSER/coq_like_pretty_printer/uris_of_filenames.pl > index.txt +echo `find . -name "*.xml"` | ~/HELM/interface/uris_of_filenames.pl > index.txt diff --git a/helm/interface/mmlinterface.ml b/helm/interface/mmlinterface.ml index d364ffe4b..06248f9ba 100755 --- a/helm/interface/mmlinterface.ml +++ b/helm/interface/mmlinterface.ml @@ -205,15 +205,41 @@ let prev rendering_window () = ;; (* 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 () = @@ -313,36 +339,41 @@ let check 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 *) @@ -519,6 +550,7 @@ object(self) (* 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)) ; @@ -581,6 +613,7 @@ object(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)) ; diff --git a/helm/interface/servers.txt b/helm/interface/servers.txt index b91a71522..a0375acd1 100644 --- a/helm/interface/servers.txt +++ b/helm/interface/servers.txt @@ -1,2 +1,3 @@ +http://cadet/helm http://caristudenti.students.cs.unibo.it/~sacerdot/helm http://pagadebit.students.cs.unibo.it/really_very_local/helm/PARSER/examples -- 2.39.2