Re: [PATCH] Document TUI mouse support in the manual & NEWS

[Eli Zaretskii <eliz@gnu.org>]

> From: Pedro Alves <pedro@palves.net>
> Cc: gdb-patches@sourceware.org
> Date: Thu, 17 Jun 2021 21:50:02 +0100
> 
> On 2021-06-17 2:17 p.m., Eli Zaretskii wrote:
> >> From: Pedro Alves <pedro@palves.net>
> >> Date: Thu, 17 Jun 2021 13:23:00 +0100
> >>
> >> +On most terminals, pressing and holding the @key{SHIFT} key on your
> >> +keyboard temporarily disables the terminal's mouse protocol, and let's
> >> +you select/paste text with the mouse.                            ^^^^^
> > 
> > Typo: should be "lets".
> > 
> > And I admit I'm confused by the above text: if one can select with the
> > mouse, why are we saying that "mouse protocol is disabled"?
> 
> How about this then:
> 
> "During normal operation, the TUI uses the terminal's mouse protocol
> and all mouse input is consumed by the TUI, which means that you
> cannot use the mouse to select/paste text, which is a terminal
> function, not a TUI function.  On most terminals however, pressing and
> holding the @key{SHIFT} key on your keyboard temporarily disables the
> terminal's mouse protocol, which then let's you select/paste text with
> the mouse."

AFAIU, what is missing here is the fact that "select/paste text with
the mouse" copies/pastes text to/from the _terminal_'s selection
buffer (as opposed to the GDB's TUI buffer).  I think your original
text will be fine if you mention this explicitly.  IOW, we need to say
that this copy/paste bypasses GDB and goes into the terminal's
text-selection functionality.

Thanks.