Re: [racket-users] DrRacket prefs?
Wow! This is great, thanks! On Thu, May 24, 2018 at 11:47 AM Robby Findlerwrote: > It may be easier to use the higher-level library, calling > preferences:set-default and preferences:set. Using that approach has > the advantage you don't need to know all of the prefs (that are > machine config and OS specific, generally), but it has the > disadvantage that you need to figure out what the right values are at > that level. But these files have some useful information: > > > https://github.com/racket/drracket/blob/master/drracket/drracket/private/main.rkt > > > https://github.com/racket/gui/blob/master/gui-lib/framework/private/main.rkt > > Here's a program that sets that particular preference (note that this > is user-specific): > > #lang racket > (require framework/preferences) > (preferences:set-default 'drracket:show-line-numbers? #t boolean?) > (preferences:set 'drracket:show-line-numbers? #t) > > Robby > > > On Thu, May 24, 2018 at 1:35 PM, Stephen Foster > wrote: > > Nice! I'll try that! > > > > On Thu, May 24, 2018 at 11:34 AM Shu-Hung You > > wrote: > >> > >> Hi Stephen, > >> > >> Running (find-system-path 'pref-file) in the REPL shows the path to > >> the preference file. Inside the file there's one line like: > >> > >> (plt:framework-pref:framework:display-line-numbers #t) > >> > >> I don't know if directly copying the pref file to another computer > >> would work but perhaps worth a try. > >> > >> > >> On Thu, May 24, 2018 at 12:28 PM, Stephen Foster > >> wrote: > >> > Hi, > >> > > >> > I know how to hide/show line numbers from within DrRacket's GUI. But > is > >> > there a way to toggle this from the command line? I have a few > hundred > >> > computers with DrRacket installed, and I want to make them all show > line > >> > numbers by default. (I'd rather not do it by hand.) > >> > > >> > Is there a command I can run or a preferences file I could edit with a > >> > script? Does anyone know where DrRacket stores user preferences like > >> > this? > >> > > >> > --Stephen > >> > > >> > -- > >> > 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. > > > > -- > > Stephen R. Foster, Ph.D., CEO > > stephenfoster.us > > multidimensionalgames.com > > learntomod.com > > vox-l.com > > thoughtstem.com > > > > -- > > 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. > -- Stephen R. Foster, Ph.D., CEO stephenfoster.us multidimensionalgames.com learntomod.com vox-l.com thoughtstem.com -- 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.
Re: [racket-users] DrRacket prefs?
It may be easier to use the higher-level library, calling preferences:set-default and preferences:set. Using that approach has the advantage you don't need to know all of the prefs (that are machine config and OS specific, generally), but it has the disadvantage that you need to figure out what the right values are at that level. But these files have some useful information: https://github.com/racket/drracket/blob/master/drracket/drracket/private/main.rkt https://github.com/racket/gui/blob/master/gui-lib/framework/private/main.rkt Here's a program that sets that particular preference (note that this is user-specific): #lang racket (require framework/preferences) (preferences:set-default 'drracket:show-line-numbers? #t boolean?) (preferences:set 'drracket:show-line-numbers? #t) Robby On Thu, May 24, 2018 at 1:35 PM, Stephen Fosterwrote: > Nice! I'll try that! > > On Thu, May 24, 2018 at 11:34 AM Shu-Hung You > wrote: >> >> Hi Stephen, >> >> Running (find-system-path 'pref-file) in the REPL shows the path to >> the preference file. Inside the file there's one line like: >> >> (plt:framework-pref:framework:display-line-numbers #t) >> >> I don't know if directly copying the pref file to another computer >> would work but perhaps worth a try. >> >> >> On Thu, May 24, 2018 at 12:28 PM, Stephen Foster >> wrote: >> > Hi, >> > >> > I know how to hide/show line numbers from within DrRacket's GUI. But is >> > there a way to toggle this from the command line? I have a few hundred >> > computers with DrRacket installed, and I want to make them all show line >> > numbers by default. (I'd rather not do it by hand.) >> > >> > Is there a command I can run or a preferences file I could edit with a >> > script? Does anyone know where DrRacket stores user preferences like >> > this? >> > >> > --Stephen >> > >> > -- >> > 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. > > -- > Stephen R. Foster, Ph.D., CEO > stephenfoster.us > multidimensionalgames.com > learntomod.com > vox-l.com > thoughtstem.com > > -- > 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.
Re: [racket-users] DrRacket prefs?
Nice! I'll try that! On Thu, May 24, 2018 at 11:34 AM Shu-Hung You < shu-hung@eecs.northwestern.edu> wrote: > Hi Stephen, > > Running (find-system-path 'pref-file) in the REPL shows the path to > the preference file. Inside the file there's one line like: > > (plt:framework-pref:framework:display-line-numbers #t) > > I don't know if directly copying the pref file to another computer > would work but perhaps worth a try. > > > On Thu, May 24, 2018 at 12:28 PM, Stephen Foster >wrote: > > Hi, > > > > I know how to hide/show line numbers from within DrRacket's GUI. But is > > there a way to toggle this from the command line? I have a few hundred > > computers with DrRacket installed, and I want to make them all show line > > numbers by default. (I'd rather not do it by hand.) > > > > Is there a command I can run or a preferences file I could edit with a > > script? Does anyone know where DrRacket stores user preferences like > this? > > > > --Stephen > > > > -- > > 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. > -- Stephen R. Foster, Ph.D., CEO stephenfoster.us multidimensionalgames.com learntomod.com vox-l.com thoughtstem.com -- 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.
Re: [racket-users] DrRacket prefs?
Hi Stephen, Running (find-system-path 'pref-file) in the REPL shows the path to the preference file. Inside the file there's one line like: (plt:framework-pref:framework:display-line-numbers #t) I don't know if directly copying the pref file to another computer would work but perhaps worth a try. On Thu, May 24, 2018 at 12:28 PM, Stephen Fosterwrote: > Hi, > > I know how to hide/show line numbers from within DrRacket's GUI. But is > there a way to toggle this from the command line? I have a few hundred > computers with DrRacket installed, and I want to make them all show line > numbers by default. (I'd rather not do it by hand.) > > Is there a command I can run or a preferences file I could edit with a > script? Does anyone know where DrRacket stores user preferences like this? > > --Stephen > > -- > 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.
[racket-users] DrRacket prefs?
Hi, I know how to hide/show line numbers from within DrRacket's GUI. But is there a way to toggle this from the command line? I have a few hundred computers with DrRacket installed, and I want to make them all show line numbers by default. (I'd rather not do it by hand.) Is there a command I can run or a preferences file I could edit with a script? Does anyone know where DrRacket stores user preferences like this? --Stephen -- 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.