indexing description: "[ A scollpanel can display another widget and provides EM_SCROLLBAR's as needed. Use `set_widget' to set the widget for the scrollbar. ]" date: "$Date$" revision: "$Revision$" class EM_SCROLLPANEL inherit EM_WIDGET export {NONE} add_widget, has_widget, remove_widget redefine make_void_surface end create make_from_widget, make_from_dimension, make_from_surface, make_void_surface feature {NONE} -- Initialisation make_from_widget (a_widget: EM_WIDGET) is -- Initialise scroll panel with `a_widget'. do make_void_surface set_widget (a_widget) resize_to_optimal_dimension end make_void_surface is -- Initialise scroll panel with void surface do create horizontal_scroll_bar.make_horizontal create vertical_scroll_bar.make_vertical create viewport_panel.make_void_surface Precursor {EM_WIDGET} add_widget (horizontal_scroll_bar) add_widget (vertical_scroll_bar) add_widget (viewport_panel) resize_event.subscribe (agent handle_widget_resized) horizontal_scroll_bar.position_changed_event.subscribe (agent handle_horizontal_position_change (?)) vertical_scroll_bar.position_changed_event.subscribe (agent handle_vertical_position_change (?)) end delegate_factory: FUNCTION [ANY, TUPLE [], like delegate] is -- Factory to create default delegate do Result := theme_delegates.scrollpanel_delegate_factory end feature -- Access widget: EM_WIDGET -- Widget displayed by `Current' horizontal_scroll_bar: EM_SCROLLBAR -- Horizontal scrollbar vertical_scroll_bar: EM_SCROLLBAR -- Vertical scrollbar viewport_panel: EM_PANEL -- Viewport to display `widget' feature -- Element change set_widget (a_widget: like widget) is -- Set `widget' to `a_widget'. do if widget /= Void then widget.resize_event.unsubscribe (agent handle_widget_resized) viewport_panel.remove_widget (widget) end widget := a_widget widget.set_border (Void) widget.set_position (0, 0) widget.resize_to_optimal_dimension viewport_panel.add_widget (widget) viewport_panel.set_background (widget.background) widget.resize_event.subscribe (agent handle_widget_resized) handle_widget_resized set_changed ensure widget_set: widget = a_widget changed: is_changed end feature {NONE} -- Implementation handle_widget_resized is -- Handle resized event of `Current' or `widget'. local viewport_width, viewport_height: INTEGER was_at_bottom: BOOLEAN do if not vertical_scroll_bar.is_visible or vertical_scroll_bar.current_value = vertical_scroll_bar.right_value then was_at_bottom := True end viewport_width := inner_width viewport_height := inner_height if widget /= Void then if widget.width > width and width > horizontal_scroll_bar.optimal_width then horizontal_scroll_bar.set_dimension (width-vertical_scroll_bar.optimal_width, horizontal_scroll_bar.optimal_height) horizontal_scroll_bar.set_position (0, height-horizontal_scroll_bar.height) horizontal_scroll_bar.set_right_value (widget.width-width+vertical_scroll_bar.width) horizontal_scroll_bar.show viewport_height := (inner_height - horizontal_scroll_bar.height).max (0) else horizontal_scroll_bar.hide end if widget.height > height and height > vertical_scroll_bar.optimal_height then vertical_scroll_bar.set_dimension (vertical_scroll_bar.optimal_width, height-horizontal_scroll_bar.optimal_height) vertical_scroll_bar.set_position (width-vertical_scroll_bar.width, 0) vertical_scroll_bar.set_right_value (widget.height-height+horizontal_scroll_bar.height) vertical_scroll_bar.show viewport_width := (inner_width - vertical_scroll_bar.width).max (0) else vertical_scroll_bar.hide end end viewport_panel.set_position (border.left, border.top) viewport_panel.set_dimension (viewport_width, viewport_height) -- TODO: add flag to set if scrollbar should be at top or bottom of center widget by default -- if vertical_scroll_bar.is_visible and was_at_bottom then -- vertical_scroll_bar.set_current_value (vertical_scroll_bar.right_value) -- end end handle_horizontal_position_change (a_value: INTEGER) is -- Handle vertical position change do if widget /= Void then widget.set_position (-a_value, widget.y) end end handle_vertical_position_change (a_value: INTEGER) is -- Handle vertical position change do if widget /= Void then widget.set_position (widget.x, -a_value) end end invariant horizontal_scroll_bar_not_void: horizontal_scroll_bar /= Void vertical_scroll_bar_not_void: vertical_scroll_bar /= Void viewport_panel_not_void: viewport_panel /= Void end