X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2FannotationHelper%2FcicAnnotationHelper.ml;h=7b150ffed238f6257a83759e653b19e283386205;hb=09aa799947c84148221af82e94e911adea8fd1e6;hp=0b858b268e5a725bd6fe60e80cd2fdcd2b68446a;hpb=8efd7ae18e1a9555e66254a39afadce56b74c42d;p=helm.git

diff --git a/helm/annotationHelper/cicAnnotationHelper.ml b/helm/annotationHelper/cicAnnotationHelper.ml
index 0b858b268..7b150ffed 100644
--- a/helm/annotationHelper/cicAnnotationHelper.ml
+++ b/helm/annotationHelper/cicAnnotationHelper.ml
@@ -45,11 +45,13 @@
 
 (* 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 "";;
 
@@ -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
@@ -210,52 +218,77 @@ let annotateb_pressed rendering_window annotation_window () =
     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 () ;
+         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
  | 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 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 *)