add a checkbox to disable online expansion in the preferences dialog

(it controls the same state as clicking in the circle in
the bottom right corner of the drracket window)
This commit is contained in:
Robby Findler 2013-01-03 10:59:43 -06:00
parent 42c77d6290
commit 12a288f135

View File

@ -2262,14 +2262,23 @@
(define parent-vp (new vertical-panel% (define parent-vp (new vertical-panel%
[parent parent] [parent parent]
[alignment '(center top)])) [alignment '(center top)]))
(new vertical-panel% [parent parent-vp])
(define vp (new vertical-panel% (define vp (new vertical-panel%
[parent parent-vp] [parent parent-vp]
[stretchable-width #f] [stretchable-width #f]
[stretchable-height #f] [stretchable-height #f]
[alignment '(left center)])) [alignment '(left center)]))
(new vertical-panel% [parent parent-vp])
(define ((make-callback pref-sym) choice evt) (define ((make-callback pref-sym) choice evt)
(preferences:set pref-sym (index->pref (send choice get-selection)))) (preferences:set pref-sym (index->pref (send choice get-selection))))
(preferences:add-check (new horizontal-panel%
[parent vp]
[stretchable-height #f]
[alignment '(center center)])
'drracket:online-compilation-default-on
(string-constant enable-online-expansion))
(new vertical-panel% [parent vp] [stretchable-height #f] [min-height 20])
(define read-choice (define read-choice
(new choice% (new choice%
[parent vp] [parent vp]
@ -2307,7 +2316,7 @@
(connect-to-prefs read-choice 'drracket:online-expansion:read-in-defs-errors) (connect-to-prefs read-choice 'drracket:online-expansion:read-in-defs-errors)
(connect-to-prefs var-choice 'drracket:online-expansion:variable-errors) (connect-to-prefs var-choice 'drracket:online-expansion:variable-errors)
(connect-to-prefs other-choice 'drracket:online-expansion:other-errors) (connect-to-prefs other-choice 'drracket:online-expansion:other-errors)
(preferences:add-check parent-vp (preferences:add-check vp
'drracket:syncheck:show-arrows? 'drracket:syncheck:show-arrows?
(string-constant show-arrows-on-mouseover)) (string-constant show-arrows-on-mouseover))
parent-vp)))) parent-vp))))