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 34c4c652002e15865e34f892c781a557a1148a9b..f838521b231333ededbac6cd0f5feaba502335d3 100644 (file)
--- 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 d0297387190ffd8bfd18ab40acccc59a7f9c7e39..04411df2b3d2e5ed394d04f33c74ac1ae5d05ace 100644 (file)
--- 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 ddf429db6d469f36a8d1542adf30ad63f0a1fcbc..b1892e64a1973fe767afb237c7285d931f5d1e95 100644 (file)
--- 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 a70b3cbe152bba2d7adb4f6ffb29443aac6da532..2d3b09afb1dcc58384ab13c77b4ee92513115e3b 100644 (file)
--- 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