]> matita.cs.unibo.it Git - helm.git/commitdiff
* Preliminary porting to ocaml-3.04 and to gdome completed.
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Wed, 27 Feb 2002 13:55:10 +0000 (13:55 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Wed, 27 Feb 2002 13:55:10 +0000 (13:55 +0000)
helm/annotationHelper/cicAnnotationHelper.ml
helm/annotationHelper/cicAnnotationHinter.ml
helm/annotationHelper/cicAnnotationHinter.mli

index 7b150ffed238f6257a83759e653b19e283386205..5ed1fa26d84a158a84f2fc4b8c892c0f801b7246 100644 (file)
@@ -57,7 +57,7 @@ let current_url = ref "";;
 
 (* GLOBAL CONSTANTS *)
 
-let helmns = Ominidom.o_mDOMString_of_string "http://www.cs.unibo.it/helm";;
+let helmns = Gdome.domString "http://www.cs.unibo.it/helm";;
 
 (* MISC FUNCTIONS *)
 
@@ -199,50 +199,65 @@ let update_output rendering_window url =
  rendering_window#output#load url
 ;;
 
-let choose_selection rendering_window (node : Ominidom.o_mDOMNode option) =
- let module O = Ominidom in
-  let rec aux node =
-   match node#get_attribute_ns (O.o_mDOMString_of_string "xref") helmns with
-     Some _ -> rendering_window#output#set_selection (Some node)
-   | None   -> aux (node#get_parent)
+let choose_selection rendering_window (element : Gdome.element option) =
+ let module G = Gdome in
+  let rec aux element =
+   if element#hasAttributeNS
+       ~namespaceURI:helmns
+       ~localName:(G.domString "xref")
+   then
+     rendering_window#output#set_selection (Some element)
+   else
+      match element#get_parentNode with
+         None -> assert false
+       (*CSC: OCAML DIVERGES!
+       | Some p -> aux (new G.element_of_node p)
+       *)
+       | Some p -> aux (new Gdome.element_of_node p)
   in
-   match node with
+   match element with
      Some x -> aux x
    | None   -> rendering_window#output#set_selection None
 ;;
 
 let annotateb_pressed rendering_window annotation_window () =
- let module O = Ominidom in
+ let module G = Gdome in
  match rendering_window#output#get_selection with
-   Some node ->
-    begin
-     match (node#get_attribute_ns (O.o_mDOMString_of_string "xref") helmns) with
-        Some xpath ->
-         let annobj = get_annotated_obj () in
-         let (anno, ids_to_targets, ids_to_annotations) = annobj in
-         let annotation = (annotation_window#annotation : GEdit.text) in
-         let id = xpath#get_string in
-          current_id := Some id ;
-          let ann = CicXPath.get_annotation ids_to_annotations id in
-           CicAnnotationHinter.create_hints annotation_window ids_to_targets
-           (xpath#get_string) ;
-           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 () ;
-     | None -> rendering_window#label#set_text ("ERROR: No xref found!!!\n")
-    end
+   Some element ->
+    let xpath =
+     ((element : Gdome.element)#getAttributeNS
+     (*CSC: OCAML DIVERGE
+     ((element : G.element)#getAttributeNS
+     *)
+       ~namespaceURI:helmns
+       ~localName:(G.domString "xref"))#to_string
+    in
+     if xpath = "" then
+      rendering_window#label#set_text ("ERROR: No xref found!!!\n")
+     else
+      let annobj = get_annotated_obj () in
+      let (anno, ids_to_targets, ids_to_annotations) = annobj in
+      let annotation = (annotation_window#annotation : GEdit.text) in
+      let id = xpath in
+       current_id := Some id ;
+       let ann = CicXPath.get_annotation ids_to_annotations id in
+        CicAnnotationHinter.create_hints annotation_window ids_to_targets
+         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 () ;
  | None -> rendering_window#label#set_text ("ERROR: No selection!!!\n")
 ;;
 
@@ -259,7 +274,7 @@ let change_annotation ids_to_annotations id ann =
 ;;
 
 (* called when the annotation is confirmed *)
-let save_annotation annotation =
+let save_annotation (annotation : GEdit.text) =
  let module S = Str in
  let module U = UriManager in
   let (annobj,ids_to_annotations) =
@@ -299,7 +314,8 @@ 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 
+let activate_t1 (output : GMathView.math_view)
+ button_set_anti_aliasing button_set_kerning 
  button_set_transparency button_export_to_postscript button_t1 ()
 =
  let is_set = button_t1#active in
@@ -341,8 +357,8 @@ let set_log_verbosity output log_verbosity_spinb () =
  output#set_log_verbosity log_verbosity_spinb#value_as_int
 ;;
 
-class settings_window output sw button_export_to_postscript
- selection_changed_callback
+class settings_window (output : GMathView.math_view)
+ sw button_export_to_postscript selection_changed_callback
 =
  let settings_window = GWindow.window ~title:"GtkMathView settings" () in
  let vbox =
@@ -398,7 +414,7 @@ object(self)
   button_set_transparency#misc#set_sensitive false ;
   (* Signals connection *)
   ignore(button_t1#connect#clicked
-   (activate_t1 output button_set_anti_aliasing button_set_kerning
+   ~callback:(activate_t1 output button_set_anti_aliasing button_set_kerning
     button_set_transparency button_export_to_postscript button_t1)) ;
   ignore(font_size_spinb#connect#changed (changefont output font_size_spinb)) ;
   ignore(button_set_anti_aliasing#connect#toggled
@@ -409,7 +425,7 @@ object(self)
    (set_transparency output button_set_transparency)) ;
   ignore(log_verbosity_spinb#connect#changed
    (set_log_verbosity output log_verbosity_spinb)) ;
-  ignore(closeb#connect#clicked settings_window#misc#hide)
+  ignore(closeb#connect#clicked ~callback:settings_window#misc#hide)
 end;;
 
 (* Main windows *)
@@ -464,7 +480,7 @@ object (self)
      true
    )) ;
   ignore (confirmb#connect#clicked
-   (fun () ->
+   ~callback:(fun () ->
      window_to_annotate#misc#hide () ;
      save_annotation annotation ;
      GMain.Grab.remove (window_to_annotate#coerce) ;
@@ -480,14 +496,14 @@ object (self)
        output#load new_current_url
    )) ;
   ignore (abortb#connect#clicked
-   (fun () ->
+   ~callback:(fun () ->
      window_to_annotate#misc#hide () ;
      GMain.Grab.remove (window_to_annotate#coerce)
    ));
   ignore (radio_some#connect#clicked
-   (fun () -> annotation#misc#set_sensitive true ; radio_some_status := true)) ;
+   ~callback:(fun () -> annotation#misc#set_sensitive true ; radio_some_status := true)) ;
   ignore (radio_none #connect#clicked
-   (fun () ->
+   ~callback:(fun () ->
      annotation#misc#set_sensitive false;
      radio_some_status := false)
    )
@@ -526,12 +542,13 @@ object(self)
 
   (* signal handlers here *)
   ignore(output#connect#selection_changed (choose_selection self)) ;
-  ignore(closeb#connect#clicked (fun _ -> GMain.Main.quit ())) ;
-  ignore(annotateb#connect#clicked (annotateb_pressed self annotation_window)) ;
+  ignore(closeb#connect#clicked ~callback:(fun _ -> GMain.Main.quit ())) ;
+  ignore(annotateb#connect#clicked
+   ~callback:(annotateb_pressed self annotation_window)) ;
   let settings_window = new settings_window output scrolled_window0
    button_export_to_postscript (choose_selection self) in
-  ignore(settingsb#connect#clicked settings_window#show) ;
-  ignore(button_export_to_postscript#connect#clicked (export_to_postscript output)) ;
+  ignore(settingsb#connect#clicked ~callback:settings_window#show) ;
+  ignore(button_export_to_postscript#connect#clicked ~callback:(export_to_postscript output)) ;
   ignore(window#event#connect#delete (fun _ -> GMain.Main.quit () ; true ))
 end;;
 
index a84b1a44d6302d8707e5e8a785b9227f31b1d894..c5acdf1241bb5762a4a17fce62e580410d1af990 100644 (file)
@@ -59,7 +59,7 @@ let link_hint annotation_window buttonno label hint =
  let button = annotation_window#annotation_hints.(buttonno) in
   sig_ids :=
    (button#connect#clicked
-    (fun () -> (annotation_window#annotation : GEdit.text)#insert hint)
+    ~callback:(fun () -> (annotation_window#annotation : GEdit.text)#insert hint)
    ) :: !sig_ids ;
   button#misc#show () ;
   match button#children with
index c21eefc88c0f2b42ff5128aa10ac1157826b8851..8cfc04c229aea119a22e15403d1b07b217b1b793 100644 (file)
@@ -36,7 +36,7 @@
 val create_hints :
   < annotation : GEdit.text;
     annotation_hints : < children : < as_widget : 'a Gtk.obj; .. > list;
-                         connect : < clicked : (unit -> unit) -> GtkSignal.id;
+                         connect : < clicked : callback:(unit -> unit) -> GtkSignal.id;
                                      .. >;
                          misc : < disconnect : GtkSignal.id -> 'b;
                                   hide : unit -> 'c; show : unit -> 'd; .. >;