lambda-term
lambda-term copied to clipboard
Add clear method to LTerm_widget.box
This PR adds a method to clear all widgets from a LTerm_widget.box.
Writing some_box#clear is easier and faster than writing
List.iter some_box#remove some_box#children
since the box only needs to be redrawn once.
I also updated my example from PR#42 to demonstrate the usage, although I'm not sure if there's any point in doing so; it's fairly self-explanatory and using #clear in this case isn't even the fastest way to do it (see the comment in double_editor.ml).