X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2FannotationHelper%2FcicAnnotationHinter.ml;h=c5acdf1241bb5762a4a17fce62e580410d1af990;hb=26992ee777bcfe3aa4d9dcd5166ff78864c8f623;hp=86bcb4588b163202ed176b4a7855d749182777d5;hpb=ff6eee275d22bd158f9ccd451aaae0cb61659a6e;p=helm.git

diff --git a/helm/annotationHelper/cicAnnotationHinter.ml b/helm/annotationHelper/cicAnnotationHinter.ml
index 86bcb4588..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
@@ -92,50 +92,50 @@ let list_mapi f =
 let get_id annterm =
  let module C = Cic in
   match annterm with
-     C.ARel (id,_,_,_)             -> id
-   | C.AVar (id,_,_)               -> id
-   | C.AMeta (id,_,_)              -> id
-   | C.ASort (id,_,_)              -> id
-   | C.AImplicit (id,_)            -> id
-   | C.ACast (id,_,_,_)            -> id
-   | C.AProd (id,_,_,_,_)          -> id
-   | C.ALambda (id,_,_,_,_)        -> id
-   | C.ALetIn (id,_,_,_,_)         -> id
-   | C.AAppl (id,_,_)              -> id
-   | C.AConst (id,_,_,_)           -> id
-   | C.AAbst (id,_,_)              -> id
-   | C.AMutInd (id,_,_,_,_)        -> id
-   | C.AMutConstruct (id,_,_,_,_,_)-> id
-   | C.AMutCase (id,_,_,_,_,_,_,_) -> id
-   | C.AFix (id,_,_,_)             -> id
-   | C.ACoFix (id,_,_,_)           -> id
+     C.ARel (id,_,_)
+   | C.AVar (id,_)
+   | C.AMeta (id,_)
+   | C.ASort (id,_)
+   | C.AImplicit id
+   | C.ACast (id,_,_)
+   | C.AProd (id,_,_,_)
+   | C.ALambda (id,_,_,_)
+   | C.ALetIn (id,_,_,_)
+   | C.AAppl (id,_)
+   | C.AConst (id,_,_)
+   | C.AAbst (id,_)
+   | C.AMutInd (id,_,_,_)
+   | C.AMutConstruct (id,_,_,_,_)
+   | C.AMutCase (id,_,_,_,_,_,_)
+   | C.AFix (id,_,_)
+   | C.ACoFix (id,_,_) -> id
 ;;
 
 let create_hint_from_term annotation_window annterm =
  let module C = Cic in
   match annterm with
-     C.ARel (id,_,_,_) ->
+     C.ARel (id,_,_) ->
       link_hints annotation_window
        [| "Binder", "<attribute name = 'binder' id = '" ^ id ^ "'/>" |]
-   | C.AVar (id,_,_) ->
+   | C.AVar (id,_) ->
       link_hints annotation_window
        [| "relURI???", "<attribute name = 'relUri' id = '" ^ id ^ "'/>" |]
-   | C.AMeta (id,_,_) ->
+   | C.AMeta (id,_) ->
       link_hints annotation_window
        [| "Number", "<attribute name = 'no' id = '" ^ id ^ "'/>" |]
-   | C.ASort (id,_,_) ->
+   | C.ASort (id,_) ->
       link_hints annotation_window
        [| "Value", "<attribute name = 'value' id = '" ^ id ^ "'/>" |]
-   | C.AImplicit (id,_) ->
+   | C.AImplicit id ->
       link_hints annotation_window [| |]
-   | C.ACast (id,_,bo,ty) ->
+   | C.ACast (id,bo,ty) ->
       let boid = get_id bo
       and tyid = get_id ty in
        link_hints annotation_window
         [| "Body", "<node id = '" ^ boid ^ "'/>" ;
            "Type", "<node id = '" ^ tyid ^ "'/>"
         |]
-   | C.AProd (id,_,_,ty,bo) ->
+   | C.AProd (id,_,ty,bo) ->
       let boid = get_id bo
       and tyid = get_id ty in
        link_hints annotation_window
@@ -144,7 +144,7 @@ let create_hint_from_term annotation_window annterm =
            "Body", "<node id = '" ^ boid ^ "'/>" ;
            "Type", "<node id = '" ^ tyid ^ "'/>"
         |]
-   | C.ALambda (id,_,_,ty,bo) ->
+   | C.ALambda (id,_,ty,bo) ->
       let boid = get_id bo
       and tyid = get_id ty in
        link_hints annotation_window
@@ -153,7 +153,7 @@ let create_hint_from_term annotation_window annterm =
            "Body", "<node id = '" ^ boid ^ "'/>" ;
            "Type", "<node id = '" ^ tyid ^ "'/>"
         |]
-   | C.ALetIn (id,_,_,ty,bo) ->
+   | C.ALetIn (id,_,ty,bo) ->
       let boid = get_id bo
       and tyid = get_id ty in
        link_hints annotation_window
@@ -162,7 +162,7 @@ let create_hint_from_term annotation_window annterm =
            "Term", "<node id = '" ^ boid ^ "'/>" ;
            "Target", "<node id = '" ^ tyid ^ "'/>"
         |]
-   | C.AAppl (id,_,args) ->
+   | C.AAppl (id,args) ->
       let argsid =
        Array.mapi
         (fun i te -> "Argument " ^ string_of_int i, "<node id ='" ^
@@ -170,19 +170,19 @@ let create_hint_from_term annotation_window annterm =
         (Array.of_list args)
       in
        link_hints annotation_window argsid
-   | C.AConst (id,_,_,_) ->
+   | C.AConst (id,_,_) ->
       link_hints annotation_window
        [| "Uri???", "<attribute name = 'uri' id = '" ^ id ^ "'/>" |]
-   | C.AAbst (id,_,_) ->
+   | C.AAbst (id,_) ->
       link_hints annotation_window
        [| "Uri???", "<attribute name = 'uri' id = '" ^ id ^ "'/>" |]
-   | C.AMutInd (id,_,_,_,_) ->
+   | C.AMutInd (id,_,_,_) ->
       link_hints annotation_window
        [| "Uri???", "<attribute name = 'uri' id = '" ^ id ^ "'/>" |]
-   | C.AMutConstruct (id,_,_,_,_,_) ->
+   | C.AMutConstruct (id,_,_,_,_) ->
       link_hints annotation_window
        [| "Uri???", "<attribute name = 'uri' id = '" ^ id ^ "'/>" |]
-   | C.AMutCase (id,_,_,_,_,outty,te,pl) ->
+   | C.AMutCase (id,_,_,_,outty,te,pl) ->
       let outtyid = get_id outty
       and teid = get_id te
       and plid =
@@ -198,7 +198,7 @@ let create_hint_from_term annotation_window annterm =
             "Term", "<node id = '" ^ teid ^ "'/>" ;
          |]
          plid)
-   | C.AFix (id,_,_,funl) ->
+   | C.AFix (id,_,funl) ->
       let funtylid =
        Array.mapi
         (fun i (_,_,ty,_) ->
@@ -233,7 +233,7 @@ let create_hint_from_term annotation_window annterm =
            [| "NoFun???", "<attribute name = 'noFun' id = '" ^ id ^ "'/>" |]
          ]
         )
-   | C.ACoFix (id,_,_,funl) ->
+   | C.ACoFix (id,_,funl) ->
       let funtylid =
        Array.mapi
         (fun i (_,ty,_) ->
@@ -267,7 +267,7 @@ let create_hint_from_term annotation_window annterm =
 let create_hint_from_obj annotation_window annobj =
  let module C = Cic in
   match annobj with
-     C.ADefinition (id,_,_,bo,ty,_) ->
+     C.ADefinition (id,_,bo,ty,_) ->
       let boid = get_id bo
       and tyid = get_id ty in
        link_hints annotation_window
@@ -276,14 +276,14 @@ let create_hint_from_obj annotation_window annobj =
            "Body", "<node id = '" ^ boid ^ "'/>" ;
            "Type", "<node id = '" ^ tyid ^ "'/>"
         |]
-   | C.AAxiom (id,_,_,ty,_) ->
+   | C.AAxiom (id,_,ty,_) ->
       let tyid = get_id ty in
        link_hints annotation_window
         [| "Name", "<attribute name = 'name' id = '" ^ id ^ "'/>" ;
            "Ingredients", "<attribute name = 'params' id = '" ^ id ^ "'/>" ;
            "Type", "<node id = '" ^ tyid ^ "'/>"
         |]
-   | C.AVariable (id,_,_,bo,ty) ->
+   | C.AVariable (id,_,bo,ty) ->
       let tyid = get_id ty in
        link_hints annotation_window
         (match bo with
@@ -298,7 +298,7 @@ let create_hint_from_obj annotation_window annobj =
                  "Type", "<node id = '" ^ tyid ^ "'/>"
               |]
         )
-   | C.ACurrentProof (id,_,_,conjs,bo,ty) ->
+   | C.ACurrentProof (id,_,conjs,bo,ty) ->
       let boid = get_id bo
       and tyid = get_id ty
       and conjsid = List.map (fun (_,te) -> get_id te) conjs in
@@ -315,7 +315,7 @@ let create_hint_from_obj annotation_window annobj =
             ) (Array.of_list conjsid)
           )
         )
-   | C.AInductiveDefinition (id,_,itl,_,_) ->
+   | C.AInductiveDefinition (id,itl,_,_) ->
       let itlids =
        List.map
         (fun (_,_,arity,cons) ->
@@ -371,7 +371,7 @@ let create_hint_from_obj annotation_window annobj =
 
 exception IdUnknown of string;;
 
-let create_hints annotation_window (annobj,ids_to_targets) xpath =
+let create_hints annotation_window ids_to_targets xpath =
  try
   match Hashtbl.find ids_to_targets xpath with
      Cic.Object annobj -> create_hint_from_obj annotation_window annobj