The "Profile" pane in DrRacket can now be dragged to resize.
This commit is contained in:
parent
760625c031
commit
b77b379534
|
@ -1548,7 +1548,7 @@ profile todo:
|
||||||
(define/override (make-root-area-container % parent)
|
(define/override (make-root-area-container % parent)
|
||||||
(set! profile-info-outer-panel
|
(set! profile-info-outer-panel
|
||||||
(super make-root-area-container
|
(super make-root-area-container
|
||||||
vertical-panel%
|
panel:vertical-dragable%
|
||||||
parent))
|
parent))
|
||||||
(make-object % profile-info-outer-panel))
|
(make-object % profile-info-outer-panel))
|
||||||
|
|
||||||
|
@ -1582,6 +1582,8 @@ profile todo:
|
||||||
(set! profile-info-visible? #t)
|
(set! profile-info-visible? #t)
|
||||||
(send profile-info-editor-canvas set-editor (send (get-current-tab) get-profile-info-text))
|
(send profile-info-editor-canvas set-editor (send (get-current-tab) get-profile-info-text))
|
||||||
(send (get-current-tab) refresh-profile)
|
(send (get-current-tab) refresh-profile)
|
||||||
|
;; set to a small percentage so it gets the minimum height
|
||||||
|
(send profile-info-outer-panel set-percentages '(9/10 1/10))
|
||||||
(update-shown)))
|
(update-shown)))
|
||||||
|
|
||||||
(field (profile-info-visible? #f))
|
(field (profile-info-visible? #f))
|
||||||
|
|
Loading…
Reference in New Issue
Block a user