suzanne.soy/racket
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

fixed bug the recording of the drscheme:htdp:last-set-teachpacks preference

Browse Source 
svn: r7012
This commit is contained in:
Robby Findler 2007-08-03 09:03:51 +00:00
parent 81136382a0
commit d5c184f893
1 changed files with 13 additions and 10 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

23
collects/lang/htdp-langs.ss
View File

@ -579,17 +579,20 @@
new-tps)))) new-tps))))
settings))) settings)))
(λ (settings name) (λ (settings name)
(make-htdp-lang-settings (let ([new-tps (filter (λ (x) (not (equal? (cadr x) name)))
(drscheme:language:simple-settings-case-sensitive settings) (htdp-lang-settings-teachpacks settings))])
(drscheme:language:simple-settings-printing-style settings) (preferences:set 'drscheme:htdp:last-set-teachpacks new-tps)
(drscheme:language:simple-settings-fraction-style settings) (make-htdp-lang-settings
(drscheme:language:simple-settings-show-sharing settings) (drscheme:language:simple-settings-case-sensitive settings)
(drscheme:language:simple-settings-insert-newlines settings) (drscheme:language:simple-settings-printing-style settings)
(drscheme:language:simple-settings-annotations settings) (drscheme:language:simple-settings-fraction-style settings)
(htdp-lang-settings-tracing? settings) (drscheme:language:simple-settings-show-sharing settings)
(filter (λ (x) (not (equal? (cadr x) name))) (drscheme:language:simple-settings-insert-newlines settings)
(htdp-lang-settings-teachpacks settings)))) (drscheme:language:simple-settings-annotations settings)
(htdp-lang-settings-tracing? settings)
new-tps)))
(λ (settings) (λ (settings)
(preferences:set 'drscheme:htdp:last-set-teachpacks '())
(make-htdp-lang-settings (make-htdp-lang-settings
(drscheme:language:simple-settings-case-sensitive settings) (drscheme:language:simple-settings-case-sensitive settings)
(drscheme:language:simple-settings-printing-style settings) (drscheme:language:simple-settings-printing-style settings)