Transformation back and forth between old and new representation

diff --git a/helm/software/components/ng_kernel/nUriManager.ml b/helm/software/components/ng_kernel/nUriManager.ml
index 40b66984571166ae7dafeaba609c12219499f2f0..3e75751c61d5abba43203cbcce7a9d47d79d1359 100644 (file)
--- 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
 ;;

diff --git a/helm/software/components/ng_kernel/nUriManager.mli b/helm/software/components/ng_kernel/nUriManager.mli
index 1e8a08cbd87435f0fab0859434ad71a000795c4f..ae8f793e66374a80c1530a41c1c77b6b30e8b2d8 100644 (file)
--- a/helm/software/components/ng_kernel/nUriManager.mli
+++ b/helm/software/components/ng_kernel/nUriManager.mli
@@ -40,5 +40,5 @@ val string_of_uri: uri -> string
 
 
 (* CACCA *)
-val nuri_of_ouri: UriManager.uri -> (int * int option ) option -> uri
+val nuri_of_ouri: UriManager.uri -> spec ->  uri
 val ouri_of_nuri: uri -> UriManager.uri