X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic%2FcicParser2.ml;h=b641c649ecd485ca20ad4c8e85d031d94e184eaa;hb=6912a028bef118d8e9d7c2847200510a9b055c6a;hp=15bc2b9350f88f090cc2a538c06bf78c8cd0e128;hpb=bac72fcaa876137ab7a5630e0c1badc2a627dce8;p=helm.git

diff --git a/helm/ocaml/cic/cicParser2.ml b/helm/ocaml/cic/cicParser2.ml
index 15bc2b935..b641c649e 100644
--- a/helm/ocaml/cic/cicParser2.ml
+++ b/helm/ocaml/cic/cicParser2.ml
@@ -40,6 +40,12 @@
 exception IllFormedXml of int;;
 exception NotImplemented;;
 
+  (* TODO ZACK implement attributes parsing from XML. ATM, parsing always
+  * returns the empty list of attributes reported here *)
+let obj_attributes = []
+let get_obj_attributes (n: 'a Pxp_document.node) =
+  obj_attributes
+
 (* Utility functions that transform a Pxp attribute into something useful *)
 
 let uri_list_of_attr a =
@@ -180,6 +186,7 @@ let rec get_term (n : CicParser3.cic_term Pxp_document.node) nbody
  let module U = UriManager in
  let module D = Pxp_document in
  let module C = Cic in
+  let obj_attrs = get_obj_attributes n in
   let ntype = n#node_type in
   match ntype with
     D.T_element "ConstantType" ->
@@ -190,7 +197,7 @@ let rec get_term (n : CicParser3.cic_term Pxp_document.node) nbody
        (match nbody with
            None ->
             (* Axiom *)
-            C.AConstant (xid, None, name, None, typ, params)
+            C.AConstant (xid, None, name, None, typ, params, obj_attrs)
          | Some nbody' ->
             let nbodytype = nbody'#node_type in
             match nbodytype with
@@ -202,7 +209,8 @@ let rec get_term (n : CicParser3.cic_term Pxp_document.node) nbody
               let xidbody = string_of_attr (nbody'#attribute "id") in
               let value = (get_content nbody')#extension#to_cic_term [] in
                if paramsbody = params then
-                C.AConstant (xid, Some xidbody, name, Some value, typ, params)
+                C.AConstant (xid, Some xidbody, name, Some value, typ, params,
+                  obj_attrs)
                else
                 raise (IllFormedXml 6)
            | D.T_element "CurrentProof" ->
@@ -212,7 +220,8 @@ let rec get_term (n : CicParser3.cic_term Pxp_document.node) nbody
               let xidbody = string_of_attr (nbody'#attribute "id") in
               let sons = nbody'#sub_nodes in
                let (conjs, value) = get_conjs_value sons in
-                C.ACurrentProof (xid, xidbody, name, conjs, value, typ, params)
+                C.ACurrentProof (xid, xidbody, name, conjs, value, typ, params,
+                  obj_attrs)
            | D.T_element _
            | D.T_data
            | _ -> raise (IllFormedXml 6)
@@ -223,7 +232,7 @@ let rec get_term (n : CicParser3.cic_term Pxp_document.node) nbody
       let inductiveTypes = get_inductive_types sons
       and params = uri_list_of_attr (n#attribute "params")
       and nparams = int_of_attr (n#attribute "noParams") in
-       C.AInductiveDefinition (xid, inductiveTypes, params, nparams)
+       C.AInductiveDefinition (xid, inductiveTypes, params, nparams, obj_attrs)
   | D.T_element "Variable" ->
      let name = string_of_attr (n#attribute "name")
      and params = uri_list_of_attr (n#attribute "params")
@@ -242,7 +251,7 @@ let rec get_term (n : CicParser3.cic_term Pxp_document.node) nbody
               (None, t'#extension#to_cic_term [])
         | _ -> raise (IllFormedXml 6)
      in
-      C.AVariable (xid,name,body,typ,params)
+      C.AVariable (xid,name,body,typ,params,obj_attrs)
   | D.T_element _
   | D.T_data
   | _ -> raise (IllFormedXml 7)