]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/components/metadata/metadataDeps.ml
- hExtlib: added debugging information for split_nth
[helm.git] / helm / software / components / metadata / metadataDeps.ml
index d34bd1c83eb9241bea1549a2f8527d583c27abd1..71fbcda7dd63286637ea783538fd71af4c4a45df 100644 (file)
@@ -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
@@ -199,13 +200,13 @@ struct
               let neighbs = UriTbl.find adjlist uri in
               if Lazy.lazy_is_val neighbs.adjacency then begin
                 let adjacency, _ =
-                  HExtlib.split_nth neighbs.shown (Lazy.force neighbs.adjacency)
+                  HExtlib.split_nth "MD 1" neighbs.shown (Lazy.force neighbs.adjacency)
                 in
                 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;
@@ -241,7 +242,7 @@ struct
             UriTbl.add adjlist dest neighborhood)
           adjacency;
         neighbs.shown <- weight;
-        fst (HExtlib.split_nth weight adjacency), weight
+        fst (HExtlib.split_nth "MD 2" weight adjacency), weight
       else begin  (* nodes has been expanded at least once *)
         let adjacency = Lazy.force neighbs.adjacency in
         let total_nodes = List.length adjacency in
@@ -250,7 +251,7 @@ struct
           let shown_before = neighbs.shown in
           neighbs.shown <- min (neighbs.shown + fat_increment) total_nodes;
           let new_shown = neighbs.shown - shown_before in
-          (fst (HExtlib.split_nth new_shown (List.rev adjacency))), new_shown
+          (fst (HExtlib.split_nth "MD 3" new_shown (List.rev adjacency))), new_shown
         end else
           [], 0 (* all children are already shown *)
       end