From 0f984fbc0271c049d86e9bcb13f315d923e6cde2 Mon Sep 17 00:00:00 2001 From: Matthew Flatt Date: Tue, 22 Jul 2008 13:28:02 +0000 Subject: [PATCH] GUI doc repairs svn: r10861 --- collects/scribblings/gui/blurbs.ss | 10 ++++++++-- collects/scribblings/gui/prefs.scrbl | 5 +++-- 2 files changed, 11 insertions(+), 4 deletions(-) diff --git a/collects/scribblings/gui/blurbs.ss b/collects/scribblings/gui/blurbs.ss index cba3bfd0cc..4e40a47d65 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 6353c82b21..38375e7070 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}).