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: 0.4.95@7852~1171 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=53f240d750e1e59bb79ce4d22de9eac23ef5f137;p=helm.git bugfix: proper computation of the amount of new node shown upon expand --- diff --git a/components/metadata/metadataDeps.ml b/components/metadata/metadataDeps.ml index c6dcd1e90..0e1dbb817 100644 --- a/components/metadata/metadataDeps.ml +++ b/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