From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Wed, 12 Jun 2002 16:09:31 +0000 (+0000)
Subject: * Abst removed from the DTD
X-Git-Tag: V_0_3_0_debian_8~47
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=2ed5c8ffbe419bdba20236d48f078f9980ed2228;p=helm.git

* Abst removed from the DTD
* Metas completely changed in the DTD
---

diff --git a/helm/annotationHelper/cicAnnotationHinter.ml b/helm/annotationHelper/cicAnnotationHinter.ml
index c5acdf124..7cf3cddbb 100644
--- a/helm/annotationHelper/cicAnnotationHinter.ml
+++ b/helm/annotationHelper/cicAnnotationHinter.ml
@@ -94,7 +94,7 @@ let get_id annterm =
   match annterm with
      C.ARel (id,_,_)
    | C.AVar (id,_)
-   | C.AMeta (id,_)
+   | C.AMeta (id,_,_)
    | C.ASort (id,_)
    | C.AImplicit id
    | C.ACast (id,_,_)
@@ -103,7 +103,6 @@ let get_id annterm =
    | C.ALetIn (id,_,_,_)
    | C.AAppl (id,_)
    | C.AConst (id,_,_)
-   | C.AAbst (id,_)
    | C.AMutInd (id,_,_,_)
    | C.AMutConstruct (id,_,_,_,_)
    | C.AMutCase (id,_,_,_,_,_,_)
@@ -120,9 +119,21 @@ let create_hint_from_term annotation_window annterm =
    | 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.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 ^ "'/>" |]
@@ -173,9 +184,6 @@ let create_hint_from_term annotation_window annterm =
    | C.AConst (id,_,_) ->
       link_hints annotation_window
        [| "Uri???", "<attribute name = 'uri' id = '" ^ id ^ "'/>" |]
-   | C.AAbst (id,_) ->
-      link_hints annotation_window
-       [| "Uri???", "<attribute name = 'uri' id = '" ^ id ^ "'/>" |]
    | C.AMutInd (id,_,_,_) ->
       link_hints annotation_window
        [| "Uri???", "<attribute name = 'uri' id = '" ^ id ^ "'/>" |]
@@ -301,8 +309,9 @@ let create_hint_from_obj annotation_window annobj =
    | 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 ^ "'/>" ;
@@ -376,6 +385,9 @@ let create_hints annotation_window ids_to_targets xpath =
   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)
 ;;