added support for customizing the edge label font to the graph library and propogated that argument to the redex traces and traces/ps functions

svn: r13155

original commit: a4799be53c07f1b3bc7dc5403d3827f8d1be7d84

collects/mrlib/graph.ss

@@ -231,6 +231,8 @@
     (mixin ((class->interface pasteboard%)) (graph-pasteboard<%>)
       (inherit find-first-snip find-next-selected-snip)
       
+      (init-field [edge-label-font #f])
+      
       (define draw-arrow-heads? #t)
       (inherit refresh get-admin)
       (define/public (set-draw-arrow-heads? x)
@@ -248,6 +250,8 @@
                     (unbox wb)
                     (unbox hb))))))
       
+      
+      
       (define arrowhead-angle-width (* 1/4 pi))
       (define arrowhead-short-side 8)
       (define arrowhead-long-side 12)
@@ -484,7 +488,12 @@
       
       (define/override (on-paint before? dc left top right bottom dx dy draw-caret)
         (when before?
-          (draw-edges dc left top right bottom dx dy))
+          (let ([old-font (send dc get-font)])
+            (when edge-label-font
+              (send dc set-font edge-label-font))
+            (draw-edges dc left top right bottom dx dy)
+            (when edge-label-font
+              (send dc set-font old-font))))
         (super on-paint before? dc left top right bottom dx dy draw-caret))
       
       (define/public (draw-edges dc left top right bottom dx dy)

collects/mrlib/scribblings/graph/graph-pasteboard-mixin.scrbl

@@ -3,5 +3,13 @@
 
 @defmixin/title[graph-pasteboard-mixin (pasteboard%) (graph-pasteboard<%>)]{
 
+@defconstructor/auto-super[([edge-label-font (or/c #f (is-a?/c font%)) #f])]{
+
+If @scheme[edge-label-font] is supplied, it is used when drawing the
+labels on the edges. Otherwise, the font is not set before drawing
+the labels, defaulting to the @scheme[dc<%>] object's font.
+
+}
+
 This mixin overrides many methods to draw lines between
 @scheme[graph-snip<%>] that it contains.}