[racket] [redex] traces for derivation trees

Hi,

As I'm enjoying the new `define-judgment-form' in Redex, I started to dream about an equivalent of `traces' for `judgment-holds'. 

I'm going to try to use Redex in a course based on Pierce's TAPL, and once students see `traces' for reduction relations, they will be a bit disappointed by the text-based output for typing derivations that one can obtain by using `current-traced-metafunctions'.

Is there something like that already? if not, does it sound feasible?

Thanks,

-- Éric