From: Claudio Sacerdoti Coen Date: Wed, 27 Feb 2002 13:55:10 +0000 (+0000) Subject: * Preliminary porting to ocaml-3.04 and to gdome completed. X-Git-Tag: V_0_3_0_debian_8~261 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=26992ee777bcfe3aa4d9dcd5166ff78864c8f623;p=helm.git * Preliminary porting to ocaml-3.04 and to gdome completed. --- diff --git a/helm/annotationHelper/cicAnnotationHelper.ml b/helm/annotationHelper/cicAnnotationHelper.ml index 7b150ffed..5ed1fa26d 100644 --- a/helm/annotationHelper/cicAnnotationHelper.ml +++ b/helm/annotationHelper/cicAnnotationHelper.ml @@ -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;; diff --git a/helm/annotationHelper/cicAnnotationHinter.ml b/helm/annotationHelper/cicAnnotationHinter.ml index a84b1a44d..c5acdf124 100644 --- a/helm/annotationHelper/cicAnnotationHinter.ml +++ b/helm/annotationHelper/cicAnnotationHinter.ml @@ -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 diff --git a/helm/annotationHelper/cicAnnotationHinter.mli b/helm/annotationHelper/cicAnnotationHinter.mli index c21eefc88..8cfc04c22 100644 --- a/helm/annotationHelper/cicAnnotationHinter.mli +++ b/helm/annotationHelper/cicAnnotationHinter.mli @@ -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; .. >;