package lambda-term
Install
dune-project
Dependency
Authors
Maintainers
Sources
sha256=3f17ccce3d214a6de868bf21f00cd66f15fd3a9a575942d93a2d614f4b9456e8
md5=9284c51c2ef18ebf6c17281879f2ff13
doc/lambda-term/LTerm_widget/class-hline/index.html
Class LTerm_widget.hlineSource
A horizontal line.
method children : t listThe children of the widget.
method parent : t optionThe parent of the widget, if any.
method set_parent : t option -> unitSets the parent of the widget. This also affect queue_draw.
method focus : t option LTerm_geom.directionsSpecify a target widget to the left, right, up and/or down when changing focus.
method set_focus : t option LTerm_geom.directions -> unitSets the target widgets when changing focus.
Enqueue a redraw operation. If the widget has a parent, this is the same as calling the queue_draw method of the parent, otherwise this does nothing.
set_queue_draw f sets the function called when the queue_draw method is invoked, for this widget and all its children.
method draw : LTerm_draw.context -> t -> unitdraw ctx focused draws the widget on the given context. focused is the focused widget.
method cursor_position : LTerm_geom.coord optionMethod invoked when the widget has the focus, it returns the position of the cursor inside the widget if it should be displayed.
method allocation : LTerm_geom.rectThe zone occuped by the widget.
method set_allocation : LTerm_geom.rect -> unitSets the zone occuped by the widget.
method send_event : LTerm_event.t -> unitSend an event to the widget. If the widget cannot process the event, it is sent to the parent and so on.
method on_event : ?switch:LTerm_widget_callbacks.switch ->
(LTerm_event.t -> bool) ->
uniton_event ?switch f calls f each time an event is received. If f returns true, the event is not passed to other callbacks.
method size_request : LTerm_geom.sizeThe size wanted by the widget.
method resources : LTerm_resources.tThe set of resources used by the widget.
method set_resources : LTerm_resources.t -> unitSets the resources of the widget and of all its children.
Sets the resource class of the widget. This can be used to set an alternative style for the widget.