]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/components/metadata/metadataDeps.ml
strange bug-fix to allow compilation on recent ocaml+camlp5o
[helm.git] / helm / software / components / metadata / metadataDeps.ml
index d34bd1c83eb9241bea1549a2f8527d583c27abd1..e6fcab592577812706ded37f667b5a21a220a7c2 100644 (file)
@@ -169,7 +169,7 @@ struct
     neighborhood UriTbl.t * UriManager.uri
       * (UriManager.uri -> UriManager.uri list) * bool
 
-  let dummy =
+  let dummy : t =
     UriTbl.create 0, UriManager.uri_of_string "cic:/a.con",
       (fun _ -> []), false
 
@@ -188,7 +188,8 @@ struct
       function
         | [] -> ()
         | uri :: tl ->
-            let suri = UriManager.string_of_uri uri in
+            let nice = UriManager.strip_xpointer in
+            let suri = UriManager.string_of_uri (nice uri) in
             Pp.node suri
               ~attrs:([ "href", UriManager.string_of_uri uri;
                         "label", label_of_uri uri
@@ -204,8 +205,8 @@ struct
                 List.iter
                   (fun dest ->
                     let uri1, uri2 = if invert then dest, uri else uri, dest in
-                    Pp.edge (UriManager.string_of_uri uri1)
-                      (UriManager.string_of_uri uri2) fmt)
+                    Pp.edge (UriManager.string_of_uri (nice uri1))
+                      (UriManager.string_of_uri (nice uri2)) fmt)
                   adjacency;
                 new_nodes := adjacency
               end;