From: Stefano Zacchiroli Date: Tue, 27 Sep 2005 14:22:15 +0000 (+0000) Subject: changed type of ids_to_uris table to (Cic.id, UriManager.uri) Hashtbl.t X-Git-Tag: V_0_7_2_3~295 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=e935206addabeeaaf03b060154335e5c3c24553a;p=helm.git changed type of ids_to_uris table to (Cic.id, UriManager.uri) Hashtbl.t (uris are no longer strings) --- diff --git a/helm/ocaml/cic_notation/cicNotationPres.ml b/helm/ocaml/cic_notation/cicNotationPres.ml index 34c4c6520..f838521b2 100644 --- a/helm/ocaml/cic_notation/cicNotationPres.ml +++ b/helm/ocaml/cic_notation/cicNotationPres.ml @@ -205,7 +205,7 @@ let render ids_to_uris = let lookup_uri id = (try let uri = Hashtbl.find ids_to_uris id in - Some uri + Some (UriManager.string_of_uri uri) with Not_found -> None) in let make_href xmlattrs xref = diff --git a/helm/ocaml/cic_notation/cicNotationPres.mli b/helm/ocaml/cic_notation/cicNotationPres.mli index d02973871..04411df2b 100644 --- a/helm/ocaml/cic_notation/cicNotationPres.mli +++ b/helm/ocaml/cic_notation/cicNotationPres.mli @@ -37,7 +37,7 @@ val box_of_mpres: mathml_markup -> boxml_markup (** level 1 -> level 0 * @param ids_to_uris mapping id -> uri for hyperlinking *) -val render: (Cic.id, string) Hashtbl.t -> CicNotationPt.term -> markup +val render: (Cic.id, UriManager.uri) Hashtbl.t -> CicNotationPt.term -> markup (** level 0 -> xml stream *) val print_xml: markup -> Xml.token Stream.t diff --git a/helm/ocaml/cic_notation/cicNotationRew.ml b/helm/ocaml/cic_notation/cicNotationRew.ml index ddf429db6..b1892e64a 100644 --- a/helm/ocaml/cic_notation/cicNotationRew.ml +++ b/helm/ocaml/cic_notation/cicNotationRew.ml @@ -36,7 +36,7 @@ type pretty_printer_id = pattern_id type term_info = { sort: (Cic.id, Ast.sort_kind) Hashtbl.t; - uri: (Cic.id, string) Hashtbl.t; + uri: (Cic.id, UriManager.uri) Hashtbl.t; } let get_types uri = @@ -297,7 +297,7 @@ let ast_of_acic0 term_info acic k = let aux = function | Cic.ARel (id,_,_,b) -> idref id (Ast.Ident (b, None)) | Cic.AVar (id,uri,substs) -> - register_uri id (UriManager.string_of_uri uri); + register_uri id uri; idref id (Ast.Ident (UriManager.name_of_uri uri, aux_substs substs)) | Cic.AMeta (id,n,l) -> idref id (Ast.Meta (n, aux_context l)) | Cic.ASort (id,Cic.Prop) -> idref id (Ast.Sort `Prop) @@ -322,19 +322,19 @@ let ast_of_acic0 term_info acic k = k s, k t)) | Cic.AAppl (aid,args) -> idref aid (Ast.Appl (List.map k args)) | Cic.AConst (id,uri,substs) -> - register_uri id (UriManager.string_of_uri uri); + register_uri id uri; idref id (Ast.Ident (UriManager.name_of_uri uri, aux_substs substs)) | Cic.AMutInd (id,uri,i,substs) as t -> let name = name_of_inductive_type uri i in let uri_str = UriManager.string_of_uri uri in let puri_str = sprintf "%s#xpointer(1/%d)" uri_str (i+1) in - register_uri id puri_str; + register_uri id (UriManager.uri_of_string puri_str); idref id (Ast.Ident (name, aux_substs substs)) | Cic.AMutConstruct (id,uri,i,j,substs) -> let name = constructor_of_inductive_type uri i j in let uri_str = UriManager.string_of_uri uri in let puri_str = sprintf "%s#xpointer(1/%d/%d)" uri_str (i + 1) j in - register_uri id puri_str; + register_uri id (UriManager.uri_of_string puri_str); idref id (Ast.Ident (name, aux_substs substs)) | Cic.AMutCase (id,uri,typeno,ty,te,patterns) -> let name = name_of_inductive_type uri typeno in @@ -578,8 +578,7 @@ let rec ast_of_acic1 term_info annterm = let idref = CicUtil.id_of_annterm annterm in (try register_uri idref - (UriManager.string_of_uri - (CicUtil.uri_of_term (Deannotate.deannotate_term annterm))) + (CicUtil.uri_of_term (Deannotate.deannotate_term annterm)) with Invalid_argument _ -> ()); idref) ctors diff --git a/helm/ocaml/cic_notation/cicNotationRew.mli b/helm/ocaml/cic_notation/cicNotationRew.mli index a70b3cbe1..2d3b09afb 100644 --- a/helm/ocaml/cic_notation/cicNotationRew.mli +++ b/helm/ocaml/cic_notation/cicNotationRew.mli @@ -28,8 +28,7 @@ val ast_of_acic: (Cic.id, CicNotationPt.sort_kind) Hashtbl.t -> (* id -> sort *) Cic.annterm -> (* acic *) CicNotationPt.term (* ast *) - * (Cic.id, string) Hashtbl.t (* id -> uri *) - (* TODO change the type of id->uri table to (Cic.id, UriManager.uri) tbl *) + * (Cic.id, UriManager.uri) Hashtbl.t (* id -> uri *) (** level 2 -> level 1 *) val pp_ast: CicNotationPt.term -> CicNotationPt.term