From 854e9a997ab127db791547efdbc3d51ca2a63d0e Mon Sep 17 00:00:00 2001 From: Robby Findler Date: Mon, 1 Sep 2014 04:11:09 -0500 Subject: [PATCH] fix dot layout when children are deleted closes PR 14718 --- pkgs/gui-pkgs/gui-lib/mrlib/private/dot.rkt | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/pkgs/gui-pkgs/gui-lib/mrlib/private/dot.rkt b/pkgs/gui-pkgs/gui-lib/mrlib/private/dot.rkt index 8f8a10603b..638b668371 100644 --- a/pkgs/gui-pkgs/gui-lib/mrlib/private/dot.rkt +++ b/pkgs/gui-pkgs/gui-lib/mrlib/private/dot.rkt @@ -86,8 +86,10 @@ snip (- (unbox rb) (unbox lb)) (- (unbox bb) (unbox tb)) - (map (λ (c) (hash-ref num-ht c)) - (send snip get-children)))))) + (filter + values + (map (λ (c) (hash-ref num-ht c #f)) + (send snip get-children))))))) children-ht))) ;; run-dot : hash-table[snip -> (list i (listof number))] string -> void