From: Stefano Zacchiroli Date: Fri, 21 Jan 2005 09:39:03 +0000 (+0000) Subject: uniformed prototype of mml_of_cic_{object,sequent} X-Git-Tag: V_0_1_0~102 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=f13dfdf18b6dcf7f9253cbd109e49891fba6fbc0;p=helm.git uniformed prototype of mml_of_cic_{object,sequent} --- diff --git a/helm/ocaml/cic_transformations/applyTransformation.ml b/helm/ocaml/cic_transformations/applyTransformation.ml index 6eff8d17b..784ab89d7 100644 --- a/helm/ocaml/cic_transformations/applyTransformation.ml +++ b/helm/ocaml/cic_transformations/applyTransformation.ml @@ -33,9 +33,6 @@ (* *) (***************************************************************************) -let reload_stylesheets = ignore -;; - let mpres_document pres_box = Ast2pres.add_xml_declaration (Box.box2xml ~obj2xml:Mpresentation.print_mpres pres_box) @@ -52,14 +49,18 @@ let mml_of_cic_sequent metasenv sequent = (ids_to_terms,ids_to_father_ids,ids_to_hypotheses) ;; -let mml_of_cic_object ~explode_all uri acic - ids_to_inner_sorts ids_to_inner_types -= +let mml_of_cic_object uri obj = + let (annobj, ids_to_terms, ids_to_father_ids, ids_to_inner_sorts, + ids_to_inner_types, ids_to_conjectures, ids_to_hypotheses) + = + Cic2acic.acic_object_of_cic_object obj + in let content = - Cic2content.annobj2content ~ids_to_inner_sorts ~ids_to_inner_types acic + Cic2content.annobj2content ~ids_to_inner_sorts ~ids_to_inner_types annobj in let pres = Content2pres.content2pres ~ids_to_inner_sorts content in let xmlpres = mpres_document pres in - Xml2Gdome.document_of_xml Misc.domImpl xmlpres -;; + let mathml = Xml2Gdome.document_of_xml Misc.domImpl xmlpres in + (mathml, + (ids_to_terms, ids_to_father_ids, ids_to_conjectures, ids_to_hypotheses)) diff --git a/helm/ocaml/cic_transformations/applyTransformation.mli b/helm/ocaml/cic_transformations/applyTransformation.mli index 4a1f08e31..1b646aa6e 100644 --- a/helm/ocaml/cic_transformations/applyTransformation.mli +++ b/helm/ocaml/cic_transformations/applyTransformation.mli @@ -33,19 +33,20 @@ (* *) (***************************************************************************) -val reload_stylesheets: unit -> unit - val mml_of_cic_sequent : - Cic.metasenv -> - int * Cic.context * Cic.term -> - Gdome.document * - ((Cic.id, Cic.term) Hashtbl.t * - (Cic.id, Cic.id option) Hashtbl.t * - (string, Cic.hypothesis) Hashtbl.t) + Cic.metasenv -> (* metasenv *) + Cic.conjecture -> (* sequent *) + Gdome.document * (* Math ML *) + ((Cic.id, Cic.term) Hashtbl.t * (* id -> term *) + (Cic.id, Cic.id option) Hashtbl.t * (* id -> father id *) + (Cic.id, Cic.hypothesis) Hashtbl.t) (* id -> hypothesis *) val mml_of_cic_object : - explode_all:bool -> - UriManager.uri -> - Cic.annobj -> - (string, string) Hashtbl.t -> - (string, Cic2acic.anntypes) Hashtbl.t -> Gdome.document + UriManager.uri -> (* object uri *) + Cic.obj -> (* uri *) + Gdome.document * (* Math ML *) + ((Cic.id, Cic.term) Hashtbl.t * (* id -> term *) + (Cic.id, Cic.id option) Hashtbl.t * (* id -> father id *) + (Cic.id, Cic.conjecture) Hashtbl.t * (* id -> conjecture *) + (Cic.id, Cic.hypothesis) Hashtbl.t) (* id -> hypothesis *) +