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) -> 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)

  The x, y, width, and height arguments specify the area that needs repainting in editor coordinates. See Caret for information about draw-caret.