mmlinterface.ml : updated to the new binding

diff --git a/helm/interface/Makefile b/helm/interface/Makefile
index d2fddf453bf4c6751910f1d402dc31f1217794a0..2697b7d521608a4122f6dd8e4126cdfa6bedc51c 100644 (file)
--- 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 17ddfc9d708b5f7b68724a166f083930a92298a0..a7d6c4d3e4ce87ecd7c928321b0716e66c8437e5 100755 (executable)
--- 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 a164883a5c47cde36bda6ee58e82a7ddea76629d..05e19f2881bb7661127862a092d9613037d3f04c 100755 (executable)
--- 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 ;