From: Luca Padovani Date: Fri, 1 Dec 2000 16:04:39 +0000 (+0000) Subject: mmlinterface.ml : updated to the new binding X-Git-Tag: nogzip~119 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=f1e359680060835d3cd2f3859fa2896a1d9ac1ae;p=helm.git mmlinterface.ml : updated to the new binding --- diff --git a/helm/interface/Makefile b/helm/interface/Makefile index d2fddf453..2697b7d52 100644 --- a/helm/interface/Makefile +++ b/helm/interface/Makefile @@ -1,8 +1,8 @@ -LABLGTK_DIR = /usr/lib/ocaml/lablgtk -LABLGTK_MATHVIEW_DIR = /usr/lib/ocaml/lablgtk/mathview -MINIDOM_DIR = /usr/lib/ocaml/minidom -PXP_DIR = /usr/lib/ocaml/site-lib/pxp -NETSTRING_DIR = /usr/lib/ocaml/site-lib/netstring +LABLGTK_DIR = /usr/local/lib/ocaml/lablgtk +LABLGTK_MATHVIEW_DIR = /usr/local/lib/ocaml/lablgtk/mathview +MINIDOM_DIR = /usr/local/lib/ocaml/minidom +PXP_DIR = /usr/local/lib/ocaml/site-lib/pxp +NETSTRING_DIR = /usr/local/lib/ocaml/site-lib/netstring 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 diff --git a/helm/interface/isterix b/helm/interface/isterix index 17ddfc9d7..a7d6c4d3e 100755 --- a/helm/interface/isterix +++ b/helm/interface/isterix @@ -3,7 +3,6 @@ # WARNING!!! No "//" in the middle of the path, nor a "/" at the end!!!! #V6.2 -#export HELM_CONFIGURATION_PREFIX=~/HELM/installation # Per (my)Coq 6.3.0 export LD_LIBRARY_PATH=/home/lpadovan/helm/usr/lib/:$LD_LIBRARY_PATH diff --git a/helm/interface/mmlinterface.ml b/helm/interface/mmlinterface.ml index a164883a5..05e19f288 100755 --- a/helm/interface/mmlinterface.ml +++ b/helm/interface/mmlinterface.ml @@ -204,33 +204,35 @@ let prev rendering_window () = rendering_window#prevb#misc#set_sensitive false ;; +exception SomethingWrong + (* called when an hyperlink is clicked *) let jump rendering_window (node : Ominidom.o_mDOMNode) = let module O = Ominidom in - let s = (node#get_attribute (O.o_mDOMString_of_string "href"))#get_string 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 + match (node#get_attribute (O.o_mDOMString_of_string "href")) with + | Some str -> + let s = str#get_string 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 + | None -> raise SomethingWrong ;; let choose_selection rendering_window (node : Ominidom.o_mDOMNode option) = let module O = Ominidom in - let rec aux node = - try - let _ = node#get_attribute (O.o_mDOMString_of_string "xref") in - rendering_window#output#set_selection node - with - O.Minidom_exception _ -> - aux (node#get_parent) - in + let rec aux node = + match node#get_attribute (O.o_mDOMString_of_string "xref") with + | Some _ -> rendering_window#output#set_selection (Some node) + | None -> aux (node#get_parent) + in match node with - None -> rendering_window#output#reset_selection - | Some node -> aux node + | Some x -> aux x + | None -> rendering_window#output#set_selection None ;; @@ -327,17 +329,16 @@ let check rendering_window () = let annotateb_pressed rendering_window annotation_window () = let module O = Ominidom in - try - let node = rendering_window#output#get_selection in - let xpath = - (node#get_attribute (O.o_mDOMString_of_string "xref"))#get_string - in - try + match rendering_window#output#get_selection with + | Some node -> + begin + match (node#get_attribute (O.o_mDOMString_of_string "xref")) with + | Some xpath -> 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 ; + ann := CicXPath.get_annotation annobj (xpath#get_string) ; + CicAnnotationHinter.create_hints annotation_window annobj (xpath#get_string) ; annotation#delete_text 0 annotation#length ; begin match !(!ann) with @@ -353,14 +354,12 @@ let annotateb_pressed rendering_window annotation_window () = end ; GMain.Grab.add (annotation_window#window_to_annotate#coerce) ; annotation_window#show () ; - with - e -> + | None -> (* 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") - with - O.Minidom_exception _ -> - (rendering_window#errors : GEdit.text)#insert "\nNo selection!\n" + errors#insert ("\nNo xref found\n") + end + | None -> (rendering_window#errors : GEdit.text)#insert "\nNo selection!\n" ;; (* called when the annotation is confirmed *) @@ -411,9 +410,8 @@ let mktree selection_changed rendering_window = (* Stuff for the widget settings *) -let export_to_postscript output () = - output#export_to_postscript ~width:595 ~height:822 ~x_margin:72 - ~y_margin:72 ~disable_colors:false "output.ps" ; +let export_to_postscript (output : GMathView.math_view) () = + output#export_to_postscript ~filename:"output.ps" (); ;; let activate_t1 output button_set_anti_aliasing button_set_kerning @@ -421,10 +419,7 @@ let activate_t1 output button_set_anti_aliasing button_set_kerning = let is_set = button_t1#active in output#set_font_manager_type - (if is_set then - GtkMathView.MathView.FontManagerT1 - else - GtkMathView.MathView.FontManagerGtk) ; + (if is_set then `font_manager_t1 else `font_manager_gtk) ; if is_set then begin button_set_anti_aliasing#misc#set_sensitive true ;