refresh in editor<%>

Repaints a region of the editor, generally called by an editor administrator. See Editors and Threads for information about edit sequences and refresh requests.

• (send an-editor refresh x y width height draw-caret background) -> void
     x : real number
     y : real number
     width : non-negative real number
     height : non-negative real number
     draw-caret : symbol in '(no-caret show-inactive-caret show-caret)
   background : color% object or #f

  The x, y, width, and height arguments specify the area that needs repainting in editor coordinates.

  See Caret for information about draw-caret.

  The background color corresponds to the background of the display; if it is #f, then the display is transparent. An editor should use the given background color as its own background (or not paint the background of background is #f).