X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FannotationHelper%2FcicAnnotationHinter.ml;h=7cf3cddbb8841b44010e1bfe03bb3afae4662ffe;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=86bcb4588b163202ed176b4a7855d749182777d5;hpb=ff6eee275d22bd158f9ccd451aaae0cb61659a6e;p=helm.git

diff --git a/helm/annotationHelper/cicAnnotationHinter.ml b/helm/annotationHelper/cicAnnotationHinter.ml
index 86bcb4588..7cf3cddbb 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,61 @@ 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.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,_,_) ->
-      link_hints annotation_window
-       [| "Number", "<attribute name = 'no' id = '" ^ id ^ "'/>" |]
-   | C.ASort (id,_,_) ->
+   | C.AMeta (id,_,subst) ->
+      let res =
+       Array.append
+        [| "Number", "<attribute name = 'no' id = '" ^ id ^ "'/>" |]
+        (Array.mapi
+          (fun i s ->
+            match s with
+               None ->
+                "Argument " ^ string_of_int i, "_"
+             | Some t ->
+                "Argument " ^ string_of_int i, "<node id ='" ^ get_id t ^ "'/>"
+          ) (Array.of_list subst)
+        )
+      in
+       link_hints annotation_window res
+   | 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 +155,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 +164,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 +173,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 +181,16 @@ let create_hint_from_term annotation_window annterm =
         (Array.of_list args)
       in
        link_hints annotation_window argsid
-   | C.AConst (id,_,_,_) ->
-      link_hints annotation_window
-       [| "Uri???", "<attribute name = 'uri' id = '" ^ id ^ "'/>" |]
-   | C.AAbst (id,_,_) ->
+   | C.AConst (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 +206,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 +241,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 +275,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 +284,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,11 +306,12 @@ 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
+      and conjsid = List.map (fun (id,_,_,_) -> id) conjs in
        link_hints annotation_window
+(*CSC: never tested since the introduction of the new Metas *)
         (Array.append
           [| "Name", "<attribute name = 'name' id = '" ^ id ^ "'/>" ;
              "Ingredients", "<attribute name = 'params' id = '" ^ id ^ "'/>" ;
@@ -315,7 +324,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,11 +380,14 @@ 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
    | Cic.Term annterm -> create_hint_from_term annotation_window annterm
+(*CSC: never tested since the introduction of the new Metas *)
+   | Cic.Hypothesis _
+   | Cic.Conjecture _ -> assert false
  with
   Not_found -> raise (IdUnknown xpath)
 ;;