From 4ba0451cafd10b58e856b52a1efbc78c6c05422f Mon Sep 17 00:00:00 2001 From: Robby Findler Date: Mon, 1 Sep 2014 10:46:37 -0500 Subject: [PATCH] make font size changes also change the font of the edge labels and the size of the arrow heads in traces closees PR 14719 --- .../redex-gui-lib/redex/private/traces.rkt | 12 +++++++++--- 1 file changed, 9 insertions(+), 3 deletions(-) diff --git a/pkgs/redex-pkgs/redex-gui-lib/redex/private/traces.rkt b/pkgs/redex-pkgs/redex-gui-lib/redex/private/traces.rkt index cf8ead8f18..79c5d34622 100644 --- a/pkgs/redex-pkgs/redex-gui-lib/redex/private/traces.rkt +++ b/pkgs/redex-pkgs/redex-gui-lib/redex/private/traces.rkt @@ -11,6 +11,7 @@ racket/gui/base racket/class racket/file + racket/math framework) (preferences:set-default 'plt-reducer:show-bottom #t boolean?) @@ -247,7 +248,7 @@ #:racket-colors? [racket-colors? #t] #:scheme-colors? [scheme-colors? racket-colors?] #:layout [layout void] - #:edge-label-font [edge-label-font #f] + #:edge-label-font [given-edge-label-font #f] #:edge-labels? [edge-labels? #t] #:filter [term-filter (lambda (x y) #t)] #:graph-pasteboard-mixin [extra-graph-pasteboard-mixin values] @@ -260,7 +261,7 @@ (define saved-parameterization (current-parameterization)) (define graph-pb (let ([pb (new (extra-graph-pasteboard-mixin graph-pasteboard%) - [layout layout] [edge-label-font edge-label-font] + [layout layout] [edge-label-font given-edge-label-font] [edge-labels? edge-labels?])]) (send pb set-flip-labels? #f) pb)) @@ -386,7 +387,12 @@ (send standard get-delta delta) (send delta set-size-mult 0) (send delta set-size-add size) - (send standard set-delta delta))) + (send standard set-delta delta) + (send graph-pb set-arrowhead-params (* pi 1/4) size (* size 2/3)) + (unless given-edge-label-font + (send graph-pb set-edge-label-font + (send the-font-list find-or-create-font + size 'default 'normal 'normal))))) ;; fill-out : (listof X) (listof X) -> (listof X) ;; produces a list whose length matches defaults but