FWIW, I have spent (far too much) time trying to replicate functionality in DrRacket that is best just used in the underlying OS or its tools somehow. One example that lives on (in a zombie-like state) is the "search in files" functionality and there are others that just died. There is definitely a tension here, but my experience suggests that it would not be a good use of my time to do something like that. At least, not without a clear pain point in my own mind. Since you see to have one of those, however, maybe you should give something a try? As Matthew pointed out, there is already command-line support (that I think doesn't get used much because it isn't very convenient to use) that you could use a starting point for wiring things in.
Robby On Thu, Nov 9, 2017 at 11:29 AM, Matthew Butterick <m...@mbtype.com> wrote: > I see your point. But this technique forfeits any broader compatibility with > desktop-oriented tools (e.g., file launchers and whatnot) > > I did try making an Automator application containing a shell script that > simply launches DrRacket, and also tried `bash -c ···` (to try to force it > to launch from inside a login session). But these didn't change the result. > > Anyhow, add it to the giant pile of things in the world that are more > complex than I thought. > > > On Nov 8, 2017, at 8:07 PM, John Clements <cleme...@brinckerhoff.org> wrote: > > On Nov 8, 2017, at 12:42, Robby Findler <ro...@eecs.northwestern.edu> wrote: > > How about "env X=Y racket -l- drracket file-to-open-in-drracket.rkt” ? > > > +1 > > > -- > 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.
