X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2Fcic2Xml.ml;h=7c674d0ad7eaab5def678e111e89a441e5372933;hb=6f6b8f33397548319fef9b374f9e9017e7fa151d;hp=f04df2f2f6bf4cce1e4b0f376723920dd9f76058;hpb=ee35bf33520d92753899985329cc4bfee141b808;p=helm.git

diff --git a/helm/gTopLevel/cic2Xml.ml b/helm/gTopLevel/cic2Xml.ml
index f04df2f2f..7c674d0ad 100644
--- a/helm/gTopLevel/cic2Xml.ml
+++ b/helm/gTopLevel/cic2Xml.ml
@@ -1,4 +1,3 @@
-
 (* Copyright (C) 2000, HELM Team.
  * 
  * This file is part of HELM, an Hypertextual, Electronic
@@ -31,7 +30,7 @@ exception NotImplemented;;
 let dtdname = "http://localhost:8081/getdtd?url=cic.dtd";;
 
 (*CSC ottimizzazione: al posto di curi cdepth (vedi codice) *)
-let print_term curi ids_to_inner_sorts =
+let print_term curi ~ids_to_inner_sorts =
  let rec aux =
   let module C = Cic in
   let module X = Xml in
@@ -116,7 +115,6 @@ let print_term curi ids_to_inner_sorts =
         let sort = Hashtbl.find ids_to_inner_sorts id in
          X.xml_empty "CONST"
           ["uri", (U.string_of_uri uri) ; "id",id ; "sort",sort]
-     | C.AAbst (id,uri) -> raise NotImplemented
      | C.AMutInd (id,uri,_,i) ->
         X.xml_empty "MUTIND"
          ["uri", (U.string_of_uri uri) ;
@@ -176,7 +174,7 @@ let print_term curi ids_to_inner_sorts =
 exception NotImplemented;;
 
 (*CSC ottimizzazione: al posto di curi cdepth (vedi codice) *)
-let print_object curi ids_to_inner_sorts =
+let print_object curi ~ids_to_inner_sorts =
  let rec aux =
   let module C = Cic in
   let module X = Xml in
@@ -185,25 +183,26 @@ let print_object curi ids_to_inner_sorts =
        C.ACurrentProof (id,n,conjectures,bo,ty) ->
         X.xml_nempty "CurrentProof" ["name",n ; "id", id]
          [< List.fold_left
-             (fun i (n,canonical_context,t) ->
+             (fun i (cid,n,canonical_context,t) ->
                [< i ;
-                  X.xml_nempty "Conjecture" ["no",(string_of_int n)]
+                  X.xml_nempty "Conjecture"
+                   ["id", cid ; "no",(string_of_int n)]
                    [< List.fold_left
-                       (fun i t ->
+                       (fun i (hid,t) ->
                          [< (match t with
                                Some (n,C.ADecl t) ->
                                 X.xml_nempty "Decl"
                                  (match n with
-                                     C.Name n' -> ["name",n']
-                                   | C.Anonimous -> [])
+                                     C.Name n' -> ["id",hid;"name",n']
+                                   | C.Anonimous -> ["id",hid])
                                  (print_term curi ids_to_inner_sorts t)
                              | Some (n,C.ADef t) ->
                                 X.xml_nempty "Def"
                                  (match n with
-                                     C.Name n' -> ["name",n']
-                                   | C.Anonimous -> [])
+                                     C.Name n' -> ["id",hid;"name",n']
+                                   | C.Anonimous -> ["id",hid])
                                  (print_term curi ids_to_inner_sorts t)
-                             | None -> X.xml_empty "Hidden" []
+                             | None -> X.xml_empty "Hidden" ["id",hid]
                             ) ;
                             i
                          >]
@@ -234,14 +233,19 @@ let print_object curi ids_to_inner_sorts =
   aux
 ;;
 
-let print_inner_types curi ids_to_inner_sorts ids_to_inner_types =
+let print_inner_types curi ~ids_to_inner_sorts ~ids_to_inner_types =
+ let module C2A = Cic2acic in
  let module X = Xml in
   X.xml_nempty "InnerTypes" ["of",UriManager.string_of_uri curi]
    (Hashtbl.fold
-     (fun id ty x ->
+     (fun id {C2A.annsynthesized = synty ; C2A.annexpected = expty} x ->
        [< x ;
           X.xml_nempty "TYPE" ["of",id]
-           (print_term curi ids_to_inner_sorts ty)
+           [< print_term curi ids_to_inner_sorts synty ;
+              match expty with
+                 None -> [<>]
+               | Some expty' -> print_term curi ids_to_inner_sorts expty'
+           >]
        >]
      ) ids_to_inner_types [<>]
    )