From: Stefano Zacchiroli Date: Thu, 20 Jul 2006 10:46:57 +0000 (+0000) Subject: bugfix: proper computation of the amount of new node shown upon expand X-Git-Tag: make_still_working~7031 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=327d441ca9c875f251c5b0aabe74f997a12075e1;p=helm.git bugfix: proper computation of the amount of new node shown upon expand --- diff --git a/helm/software/components/metadata/metadataDeps.ml b/helm/software/components/metadata/metadataDeps.ml index c6dcd1e90..0e1dbb817 100644 --- a/helm/software/components/metadata/metadataDeps.ml +++ b/helm/software/components/metadata/metadataDeps.ml @@ -188,17 +188,18 @@ struct adjacency; neighbs.shown <- weight; fst (HExtlib.split_nth weight adjacency), weight - else (* nodes has been expanded at least once *) + else begin (* nodes has been expanded at least once *) let adjacency = Lazy.force neighbs.adjacency in let total_nodes = List.length adjacency in if neighbs.shown < total_nodes then begin (* some more children to show ... *) let shown_before = neighbs.shown in neighbs.shown <- min (neighbs.shown + fat_increment) total_nodes; - let new_shown = shown_before - neighbs.shown in + let new_shown = neighbs.shown - shown_before in (fst (HExtlib.split_nth new_shown (List.rev adjacency))), new_shown end else [], 0 (* all children are already shown *) + end with Not_found -> (*eprintf "uri not found: %s\n%!" (UriManager.string_of_uri uri);*) [], 0