X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Furimanager%2FuriManager.ml;h=00cf4faa7a4775409eabdcb4d8610c9278a73329;hb=fdd8107cc53f5e862004aa5fcd48593ee5634234;hp=6dad8ddef6c4095e4764497f21150d53c4e649e2;hpb=0d436761ba03acfadbfe913c0a38367068bdbb47;p=helm.git

diff --git a/helm/ocaml/urimanager/uriManager.ml b/helm/ocaml/urimanager/uriManager.ml
index 6dad8ddef..00cf4faa7 100644
--- a/helm/ocaml/urimanager/uriManager.ml
+++ b/helm/ocaml/urimanager/uriManager.ml
@@ -23,17 +23,29 @@
  * http://cs.unibo.it/helm/.
  *)
 
-(* "cic:/a/b/c.con" => [| "cic:/a" ; "cic:/a/b" ; "cic:/a/b/c.con" ; "c" |] *)
+(*
+* "cic:/a/b/c.con" => [| "cic:/a" ; "cic:/a/b" ; "cic:/a/b/c.con" ; "c"; "" |]
+* "cic:/a/b/c.ind#xpointer(1/1)" =>
+*   [| "cic:/a" ; "cic:/a/b" ; "cic:/a/b/c.con" ; "c"; "#xpointer(1/1)" |]
+* "cic:/a/b/c.ind#xpointer(1/1/1)" =>
+*   [| "cic:/a" ; "cic:/a/b" ; "cic:/a/b/c.con" ; "c"; "#xpointer(1/1/1)" |]
+*)
 type uri = string array;;
 
 let eq uri1 uri2 =
  uri1 == uri2
 ;;
 
-let string_of_uri uri = uri.(Array.length uri - 2);;
-let name_of_uri uri = uri.(Array.length uri - 1);;
-let buri_of_uri uri = uri.(Array.length uri - 3);;
-let depth_of_uri uri = Array.length uri - 2;;
+let string_of_uri uri =
+  match  uri.(Array.length uri - 1) with
+  | "" -> 
+      uri.(Array.length uri - 3)
+  | _ -> 
+      String.concat "#" 
+        [ uri.(Array.length uri - 3); uri.(Array.length uri - 1) ]
+let name_of_uri uri = uri.(Array.length uri - 2);;
+let buri_of_uri uri = uri.(Array.length uri - 4);;
+let depth_of_uri uri = Array.length uri - 3;;
 
 module OrderedStrings =
  struct
@@ -62,12 +74,12 @@ let normalize prefix =
 
 exception IllFormedUri of string;;
 
-let mk_prefixes str =
+let mk_prefixes str xpointer =
  let rec aux curi =
   function
      [he] ->
       let prefix_uri = curi ^ "/" ^ he
-      and name = List.hd (Str.split (Str.regexp "\.") he) in
+      and name = List.hd (Str.split (Str.regexp "\\.") he) in
        [ normalize prefix_uri ; name ]
    | he::tl ->
       let prefix_uri = curi ^ "/" ^ he in
@@ -81,52 +93,70 @@ let mk_prefixes str =
      with Failure "hd" | Failure "tl" ->
       raise (IllFormedUri str))
     in
-    aux ty sp
+    (aux ty sp) @ [xpointer]
+;;
+
+
+let sharp_rex = 
+  Str.regexp "#"
 ;;
 
 let uri_of_string str =
- try
-  SetOfStrings.find str !set_of_uri
- with
-  Not_found ->
-   let uri = Array.of_list (mk_prefixes str) in
-    set_of_uri := SetOfStrings.add str uri !set_of_uri ;
-    uri
+  let base, xpointer =
+    match Str.split sharp_rex str with
+    | [base] -> base,""
+    | [base; xpointer] -> base,xpointer 
+    | _ -> raise (IllFormedUri str)
+  in
+   try
+    SetOfStrings.find str !set_of_uri
+   with
+    Not_found ->
+      let uri = Array.of_list (mk_prefixes base xpointer) in
+      set_of_uri := SetOfStrings.add str uri !set_of_uri ;
+      uri
 ;;
 
+let strip_xpointer uri =
+  let stripped_uri = Array.copy uri in
+  stripped_uri.(Array.length uri - 1) <- "";  (* reset xpointer field *)
+  let stripped_uri_str = string_of_uri stripped_uri in
+  set_of_uri := SetOfStrings.add stripped_uri_str stripped_uri !set_of_uri;
+  stripped_uri
+
 let cicuri_of_uri uri =
  let completeuri = string_of_uri uri in
   let newcompleteuri = 
-   (Str.replace_first (Str.regexp "\.types$") ""
-    (Str.replace_first (Str.regexp "\.ann$") "" completeuri))
+   (Str.replace_first (Str.regexp "\\.types$") ""
+    (Str.replace_first (Str.regexp "\\.ann$") "" completeuri))
   in
    if completeuri = newcompleteuri then
     uri
    else
     let newuri = Array.copy uri in
-     newuri.(Array.length uri - 2) <- newcompleteuri ;
+     newuri.(Array.length uri - 3) <- newcompleteuri ;
      newuri
 ;;
 
 let annuri_of_uri uri =
  let completeuri = string_of_uri uri in
-  if Str.string_match (Str.regexp ".*\.ann$") completeuri 0 then
+  if Str.string_match (Str.regexp ".*\\.ann$") completeuri 0 then
    uri
   else
    let newuri = Array.copy uri in
-    newuri.(Array.length uri - 2) <- completeuri ^ ".ann" ;
+    newuri.(Array.length uri - 3) <- completeuri ^ ".ann" ;
     newuri
 ;;
 
 let uri_is_annuri uri =
- Str.string_match (Str.regexp ".*\.ann$") (string_of_uri uri) 0
+ Str.string_match (Str.regexp ".*\\.ann$") (string_of_uri uri) 0
 ;;
 
 let bodyuri_of_uri uri =
  let struri = string_of_uri uri in
-  if Str.string_match (Str.regexp ".*\.con$") (string_of_uri uri) 0 then
+  if Str.string_match (Str.regexp ".*\\.con$") (string_of_uri uri) 0 then
    let newuri = Array.copy uri in
-    newuri.(Array.length uri - 2) <- struri ^ ".body" ;
+    newuri.(Array.length uri - 3) <- struri ^ ".body" ;
     Some newuri
   else
    None
@@ -135,6 +165,17 @@ let bodyuri_of_uri uri =
 let innertypesuri_of_uri uri =
  let cicuri = cicuri_of_uri uri in
   let newuri = Array.copy cicuri in
-   newuri.(Array.length cicuri - 2) <- (string_of_uri cicuri) ^ ".types" ;
+   newuri.(Array.length cicuri - 3) <- (string_of_uri cicuri) ^ ".types" ;
    newuri
 ;;
+
+type uriref = uri * (int list)
+
+let string_of_uriref (uri, fi) =
+   let str = string_of_uri uri in
+   let xp t = "#xpointer(1/" ^ string_of_int (t + 1) in
+   match fi with
+      | []          -> str 
+      | [t]         -> str ^ xp t ^ ")" 
+      | t :: c :: _ -> str ^ xp t ^ "/" ^ string_of_int c ^ ")" 
+