X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Finterface%2Fmmlinterface.ml;h=06248f9ba61062d726cb60ae04786dd36bb31730;hb=e6a36a24f7c27739067073172a387b85cd0a6c5c;hp=d364ffe4b0257efbff9d48eb0da54a8742f83741;hpb=60e11bd6b405601316548ec7b063e3fb59bd4d07;p=helm.git

diff --git a/helm/interface/mmlinterface.ml b/helm/interface/mmlinterface.ml
index d364ffe4b..06248f9ba 100755
--- a/helm/interface/mmlinterface.ml
+++ b/helm/interface/mmlinterface.ml
@@ -205,15 +205,41 @@ let prev rendering_window () =
 ;;
 
 (* called when an hyperlink is clicked *)
-let jump rendering_window s =
- 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
+let jump rendering_window node =
+ let module M = Minidom in
+  let s =
+   match M.node_get_attribute node (M.mDOMString_of_string "href") with
+      None   -> assert false
+    | Some s -> M.string_of_mDOMString s
+  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
+;;
+
+let choose_selection rendering_window node =
+ let module M = Minidom in
+ let rec aux ~first_time node =
+  match M.node_get_attribute node (M.mDOMString_of_string "xref") with
+     None ->
+      let parent =
+       match M.node_get_parent node with
+          None -> assert false
+        | Some parent -> parent
+      in
+       aux ~first_time:false parent
+   | Some s ->
+      if not first_time then
+       rendering_window#output#set_selection (Some node)
+ in
+  match node with
+     None      -> () (* No element selected *)
+   | Some node -> aux ~first_time:true node
 ;;
 
 let changefont rendering_window () =
@@ -313,36 +339,41 @@ let check rendering_window () =
 ;;
 
 let annotateb_pressed rendering_window annotation_window () =
- let xpath = (rendering_window#output#get_selection : string option) in
-  match xpath with
-     None -> (rendering_window#errors : GEdit.text)#insert "\nNo selection!\n"
-   | Some xpath ->
-    try
-     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 ;
-      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 () ;
-    with
-      e ->
+ let module M = Minidom in
+ match rendering_window#output#get_selection with
+    None -> (rendering_window#errors : GEdit.text)#insert "\nNo selection!\n"
+  | Some node ->
+     let xpath =
+      match M.node_get_attribute node (M.mDOMString_of_string "xref") with
+         None -> assert false
+       | Some xpath -> M.string_of_mDOMString xpath
+     in
+      try
+       let annobj = get_annotated_obj ()
        (* 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")
+       and annotation = (annotation_window#annotation : GEdit.text) in
+        ann := CicXPath.get_annotation annobj xpath ;
+        CicAnnotationHinter.create_hints annotation_window annobj 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 () ;
+      with
+        e ->
+         (* 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")
 ;;
 
 (* called when the annotation is confirmed *)
@@ -519,6 +550,7 @@ object(self)
 
   (* signal handlers here *)
   ignore(output#connect#jump (jump self)) ;
+  ignore(output#connect#selection_changed (choose_selection self)) ;
   ignore(nextb#connect#clicked (next self)) ;
   ignore(prevb#connect#clicked (prev self)) ;
   ignore(checkb#connect#clicked (check self)) ;
@@ -581,6 +613,7 @@ object(self)
 
   (* signal handlers here *)
   ignore(output#connect#jump (jump rendering_window)) ;
+  ignore(output#connect#selection_changed (choose_selection self)) ;
   ignore(nextb#connect#clicked (theory_next self)) ;
   ignore(prevb#connect#clicked (theory_prev self)) ;
   ignore(checkb#connect#clicked (theory_check self)) ;