There's not a simple way to do that right now, but I think a change to the code to make that more configurable would be great.
It is probably best to make this as a change to DrRacket proper and support a cleaner interface all around. It might be nice to be able to click on things in the interactions window to change the set that will be run next time, for example. I've been thinking that this needs cleanup but haven't find time to actually do it, sadly. Robby On Tue, Jan 24, 2017 at 11:13 AM, Laurent <laurent.ors...@gmail.com> wrote: > Hi all, > > Currently we can choose what submodules to run via the 'Choose Language...' > settings. > > I'd like to make a keyboard shortcut that executes the current module but > first asks the user what submodules she wants to run. > > So far I found > (add-drs-function "run" (λ (frame) (send frame execute-callback))) > https://github.com/racket/drracket/blob/da4d2db396290edebee0e87908a0ff265c4c6f3a/drracket/drracket/private/rep.rkt#L213 > > and the 'execute-callback': > https://github.com/racket/drracket/blob/da4d2db396290edebee0e87908a0ff265c4c6f3a/drracket/drracket/private/unit.rkt#L2854 > > But it seems that what submodules are run may be buried in > 'module-language-settings'. Or is there a simple way to dynamically override > these settings, say with an argument to 'execute-callback'? > > If that's too difficult, as a workaround I could go with running the module > without any submodule---so I can choose afterwards what submodules to enter. > > Thanks, > Laurent > > -- > You received this message because you are subscribed to the Google Groups > "Racket Users" group. > To unsubscribe from this group and stop receiving emails from it, send an > email to racket-users+unsubscr...@googlegroups.com. > For more options, visit https://groups.google.com/d/optout. -- You received this message because you are subscribed to the Google Groups "Racket Users" group. To unsubscribe from this group and stop receiving emails from it, send an email to racket-users+unsubscr...@googlegroups.com. For more options, visit https://groups.google.com/d/optout.
