X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FannotationHelper%2FcicAnnotationHelper.ml;h=5ed1fa26d84a158a84f2fc4b8c892c0f801b7246;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=0b858b268e5a725bd6fe60e80cd2fdcd2b68446a;hpb=8efd7ae18e1a9555e66254a39afadce56b74c42d;p=helm.git diff --git a/helm/annotationHelper/cicAnnotationHelper.ml b/helm/annotationHelper/cicAnnotationHelper.ml index 0b858b268..5ed1fa26d 100644 --- a/helm/annotationHelper/cicAnnotationHelper.ml +++ b/helm/annotationHelper/cicAnnotationHelper.ml @@ -45,17 +45,19 @@ (* GLOBAL REFERENCES (USED BY CALLBACKS) *) -let annotated_obj = ref None;; (* reference to a couple option where *) +let annotated_obj = ref None;; (* reference to a triple option where *) (* the first component is the current *) - (* annotated object and the second is *) - (* the map from ids to annotated targets *) -let ann = ref (ref None);; (* current annotation *) + (* annotated object, the second is the *) + (* map from ids to annotated targets and *) + (* the third is the map from ids to *) + (* annotations. *) +let current_id = ref None;; (* id of the element to annotate *) let radio_some_status = ref false;; (* is the radio_some button selected? *) 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 *) @@ -179,7 +181,13 @@ let get_annotated_obj () = match !annotated_obj with None -> let annobj = - (CicCache.get_annobj (get_current_uri ())) + let (annobj,ids_to_annotations) = + match CicCache.get_annobj (get_current_uri ()) with + (annobj,None) -> annobj, Hashtbl.create 503 + | (annobj, Some ids_to_annotations) -> (annobj,ids_to_annotations) + in + let ids_to_targets = CicXPath.get_ids_to_targets annobj in + (annobj,ids_to_targets,ids_to_annotations) in annotated_obj := Some annobj ; annobj @@ -191,71 +199,111 @@ 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 () - and annotation = (annotation_window#annotation : GEdit.text) in - 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 - 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") ;; +let change_annotation ids_to_annotations id ann = + begin + try + Hashtbl.remove ids_to_annotations id + with + Not_found -> () + end ; + match ann with + None -> () + | Some ann' -> Hashtbl.add 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 - if !radio_some_status then - !ann := Some (annotation#get_chars 0 annotation#length) - else - !ann := None ; - match !annotated_obj with - None -> assert false - | Some (annobj,_) -> - let uri = get_current_uri () in - let annxml = CicAnnotation2Xml.pp_annotation annobj uri in - make_dirs - (pathname_of_annuri (U.buri_of_uri uri)) ; - Xml.pp ~quiet:true annxml - (Some - (pathname_of_annuri (U.string_of_uri (U.annuri_of_uri uri)) ^ - ".xml" - ) - ) + let (annobj,ids_to_annotations) = + match !annotated_obj with + None -> assert false + | Some (annobj,_,ids_to_annotations) -> annobj,ids_to_annotations + in + change_annotation ids_to_annotations + (match !current_id with + Some id -> id + | None -> assert false + ) + (if !radio_some_status then + Some (annotation#get_chars 0 annotation#length) + else + None + ) ; + let uri = get_current_uri () in + let annxml = + CicAnnotation2Xml.pp_annotation annobj ids_to_annotations uri + in + make_dirs + (pathname_of_annuri (U.buri_of_uri uri)) ; + Xml.pp ~quiet:true annxml + (Some + (pathname_of_annuri (U.string_of_uri (U.annuri_of_uri uri)) ^ + ".xml" + ) + ) ;; (* STUFF TO BUILD THE GTK INTERFACE *) @@ -266,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 @@ -308,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 = @@ -365,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 @@ -376,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 *) @@ -431,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) ; @@ -447,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) ) @@ -493,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;;