diff --git a/collects/scribblings/gui/blurbs.ss b/collects/scribblings/gui/blurbs.ss index cba3bfd0..4e40a47d 100644 --- a/collects/scribblings/gui/blurbs.ss +++ b/collects/scribblings/gui/blurbs.ss @@ -253,11 +253,17 @@ information@|details|, even if the editor currently has delayed refreshing (see (hspace 1) (bytes->string/latin-1 name)))) + (define (res-sym s) + (string->symbol (string-append "MrEd:" s))) + (define (Resource s) - @elem{@to-element[`(quote ,(string->symbol (string-append "MrEd:" s)))] + @elem{@to-element[`(quote ,(res-sym s))] preference}) (define (ResourceFirst s) ; fixme -- add index - (Resource s)) + (let ([r (Resource s)]) + (index* (list (format "~a preference" (res-sym s))) + (list r) + r))) (define (edsnipsize a b c) @elem{An @scheme[editor-snip%] normally stretches to wrap around the size diff --git a/collects/scribblings/gui/prefs.scrbl b/collects/scribblings/gui/prefs.scrbl index 6353c82b..38375e70 100644 --- a/collects/scribblings/gui/prefs.scrbl +++ b/collects/scribblings/gui/prefs.scrbl @@ -1,5 +1,6 @@ #lang scribble/doc -@(require "common.ss") +@(require "common.ss" + (for-label scheme/file)) @title[#:tag "mredprefs"]{Preferences} @@ -7,7 +8,7 @@ MrEd supports a number of preferences for global configuration. The MrEd preferences are stored in the common file reported by @scheme[find-system-path] for @indexed-scheme['pref-file], and preference values can be retrieved and changed through - @scheme[get-preference] and @scheme[set-preference]. However, MrEd + @scheme[get-preference] and @scheme[put-preferences]. However, MrEd reads most preferences once at startup (all except the @Resource{playcmd}).