From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Thu, 31 Jan 2008 14:50:19 +0000 (+0000)
Subject: snapshot]
X-Git-Tag: make_still_working~5646
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=71303c30466f24b8953def22a80175c00dd975af;p=helm.git

snapshot]
---

diff --git a/helm/software/components/ng_kernel/nUriManager.ml b/helm/software/components/ng_kernel/nUriManager.ml
index de7116cb1..95e3271b1 100644
--- a/helm/software/components/ng_kernel/nUriManager.ml
+++ b/helm/software/components/ng_kernel/nUriManager.ml
@@ -23,18 +23,59 @@
  * http://cs.unibo.it/helm/.
  *)
 
-exception IllFormedUri of string Lazy.t;;
+(*                order, uri,      (which, constructor)        *)
+type uri = Uri of int *  string *  (int  * int option ) option
 
-(*                        order, uri,      (type, constructor)        *)
-type uri = private Uri of int *  string *  (int * int option ) option
-
-let eq (Uri(_,x1,x2)) (Uri(_,y1,y2)) = x1 = y1 && x2 = y2;;
+let eq = (==);;
 
 let string_of_uri = function
   | Uri (_,s,None) -> s
   | Uri (_,s,Some (i,None)) -> 
       s ^ "#xpointer(1/" ^ string_of_int (i+1) ^ ")"
   | Uri (_,s,Some (i, Some k)) -> 
-      s ^ "#xpointer(1/" ^ string_of_int (i+1) ^ "/" ^ string_of_int k ^ ")"
+      s ^ "#xpointer(1/" ^ string_of_int (i+1) ^ "/" ^ string_of_int (k+1) ^ ")"
+;;
+
+module OrderedStrings =
+ struct
+  type t = string
+  let compare (s1 : t) (s2 : t) = compare s1 s2
+ end
+;;
+
+module MapStringsToUri = Map.Make(OrderedStrings);;
+
+let set_of_uri = ref MapStringsToUri.empty;;
+
+let uri_of_string_aux =
+  let counter = ref 0 in fun s ->
+  incr counter;
+  try
+    let sharp = String.rindex s '#' in
+    let pre = String.sub s 0 sharp in
+    let ind = String.sub s (sharp+12) (String.length s - (sharp+13)) in
+    try
+      let slash = String.rindex ind '/' in
+      let indno = String.sub ind 0 slash in   
+      let constr = String.sub ind (slash+1) (String.length ind - (slash+1)) in
+      Uri(!counter,pre,Some(int_of_string indno-1,Some(int_of_string constr-1)))
+    with Not_found -> Uri (!counter,pre,Some (int_of_string ind-1, None))
+  with Not_found -> Uri (!counter,s,None)
+;;
+
+let uri_of_string s =
+  try
+    MapStringsToUri.find s !set_of_uri
+  with Not_found ->
+    let new_uri = uri_of_string_aux s in
+    set_of_uri := MapStringsToUri.add s new_uri !set_of_uri;
+    new_uri
 ;;
 
+let nuri_of_ouri u indinfo =
+  uri_of_string (string_of_uri (Uri(0,UriManager.string_of_uri u,indinfo)))
+;;
+
+let ouri_of_nuri u =
+  UriManager.uri_of_string (string_of_uri u)
+;;
diff --git a/helm/software/components/ng_kernel/nUriManager.mli b/helm/software/components/ng_kernel/nUriManager.mli
index b05ae502c..9823719c3 100644
--- a/helm/software/components/ng_kernel/nUriManager.mli
+++ b/helm/software/components/ng_kernel/nUriManager.mli
@@ -23,12 +23,14 @@
  * http://cs.unibo.it/helm/.
  *)
 
-exception IllFormedUri of string Lazy.t;;
-
-(*                        order, uri,      (type, constructor)        *)
-type uri = private Uri of int *  string *  (int * int option ) option
+(*                        order, uri,      (which, constructor)        *)
+type spec = Normal of (int  * int option) option | 
+type uri = private Uri of int *  string * spec
 
 val eq: uri -> uri -> bool
-
 val string_of_uri: uri -> string 
 
+
+(* CACCA *)
+val nuri_of_ouri: UriManager.uri -> (int * int option ) option -> uri
+val ouri_of_nuri: uri -> UriManager.uri