From: Stefano Zacchiroli <zack@upsilon.cc>
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