X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fcomponents%2Fng_kernel%2FnUriManager.ml;h=3e75751c61d5abba43203cbcce7a9d47d79d1359;hb=1df7f33eaed35696773168dedf9eb1c952a57c19;hp=40b66984571166ae7dafeaba609c12219499f2f0;hpb=eac47b8c4a4e136507d82f2cc16b2d0c5093d710;p=helm.git

diff --git a/helm/software/components/ng_kernel/nUriManager.ml b/helm/software/components/ng_kernel/nUriManager.ml
index 40b669845..3e75751c6 100644
--- a/helm/software/components/ng_kernel/nUriManager.ml
+++ b/helm/software/components/ng_kernel/nUriManager.ml
@@ -95,9 +95,31 @@ fun s ->
 ;;
 
 let nuri_of_ouri u indinfo =
-  uri_of_string (string_of_uri (Uri(0,UriManager.string_of_uri u,indinfo)))
+  let s = UriManager.string_of_uri u in
+  let dot = String.rindex s '.' in
+  let s2 = String.sub s 0 dot in
+  let ns = match indinfo with
+  | Decl ->  s2 ^ ".dec"
+  | Def -> s2 ^ ".def"
+  | Fix (i,j)  -> s2 ^ ".fix(" ^ string_of_int i ^ "," ^ string_of_int j ^ ")"
+  | 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
 ;;
 
 let ouri_of_nuri u =
-  UriManager.uri_of_string (string_of_uri u)
+  let s = string_of_uri 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
+  let os =  
+    match suffix with
+    | "dec" 
+    | "def" -> prefix ^ ".con"
+    | "ind" 
+    | "con" -> prefix ^ ".ind"
+    | _ -> assert false
+  in
+  UriManager.uri_of_string os
 ;;