AnnotateGPT: Designing Human–AI Collaboration in Pen-Based Document Annotation.