uri -> reference

[helm.git] / helm / software / components / ng_kernel / nUriManager.ml

diff --git a/helm/software/components/ng_kernel/nUriManager.ml b/helm/software/components/ng_kernel/nUriManager.ml
index 3e75751c61d5abba43203cbcce7a9d47d79d1359..745f9359c6f44cf61eb836fcc743493ea1f1d68e 100644 (file)
--- a/helm/software/components/ng_kernel/nUriManager.ml
+++ b/helm/software/components/ng_kernel/nUriManager.ml
@@ -23,7 +23,7 @@
  * http://cs.unibo.it/helm/.
  *)
 
-exception IllFormedUri of string Lazy.t
+exception IllFormedReference of string Lazy.t
 
 type spec = 
  | Decl 
@@ -33,11 +33,11 @@ type spec =
  | Ind of int
  | Con of int * int (* indtyno, constrno *)
 
-type uri = Uri of int * string * spec
+type reference = Ref of int * string * spec
 
 let eq = (==);;
 
-let string_of_uri (Uri (_,s,_)) = s;;
+let string_of_reference (Uri (_,s,_)) = s;;
 
 module OrderedStrings =
  struct
@@ -48,7 +48,7 @@ module OrderedStrings =
 
 module MapStringsToUri = Map.Make(OrderedStrings);;
 
-let set_of_uri = ref MapStringsToUri.empty;;
+let set_of_reference = ref MapStringsToUri.empty;;
 
 (* '.' not allowed in path and foo
  *
@@ -60,7 +60,7 @@ let set_of_uri = ref MapStringsToUri.empty;;
  * Con of int * int       cic:/path/foo.con(i,j)
  *)
 
-let uri_of_string =
+let reference_of_string =
   let counter = ref 0 in 
   let c () = incr counter; !counter in 
   let get2 s dot =
@@ -74,9 +74,9 @@ let uri_of_string =
     i
   in
 fun s ->
-  try MapStringsToUri.find s !set_of_uri
+  try MapStringsToUri.find s !set_of_reference
   with Not_found ->
-    let new_uri =
+    let new_reference =
       try
         let dot = String.rindex s '.' in
         let suffix = String.sub s (dot+1) 3 in
@@ -90,11 +90,11 @@ fun s ->
         | _ -> raise Not_found
       with Not_found -> raise (IllFormedUri (lazy s))
     in
-    set_of_uri := MapStringsToUri.add s new_uri !set_of_uri;
-    new_uri
+    set_of_reference := MapStringsToUri.add s new_reference !set_of_reference;
+    new_reference
 ;;
 
-let nuri_of_ouri u indinfo =
+let reference_of_ouri u indinfo =
   let s = UriManager.string_of_uri u in
   let dot = String.rindex s '.' in
   let s2 = String.sub s 0 dot in
@@ -105,11 +105,11 @@ let nuri_of_ouri u indinfo =
   | CoFix i -> s2 ^ ".cfx(" ^ string_of_int i ^ ")"
   | Ind i -> s2 ^ ".ind(" ^ string_of_int i ^ ")"
   | Con (i,j) -> s2 ^ ".con(" ^ string_of_int i ^ "," ^ string_of_int j ^ ")"
-  in uri_of_string ns
+  in reference_of_string ns
 ;;
 
-let ouri_of_nuri u =
-  let s = string_of_uri u in
+let ouri_of_reference u =
+  let s = string_of_reference u in
   let dot = String.rindex s '.' in
   let prefix = String.sub s 0 dot in
   let suffix = String.sub s (dot+1) 3 in