Re: [PATCH] Add "set style tui-current-position on|off" default to off

[Eli Zaretskii <eliz@gnu.org>]

> Date: Tue, 16 Jun 2020 12:02:31 +0100
> From: Pedro Alves via Gdb-patches <gdb-patches@sourceware.org>
> Cc: Tom Tromey <tom@tromey.com>,
>  Pedro Alves via Gdb-patches <gdb-patches@sourceware.org>
> 
> gdb/ChangeLog:
> 
> 	* NEWS: Document that the TUI no longer styles the source code
> 	highlighted by the current position indicator by default.
> 	Mention "set style tui-current-position".
> 
> 	* cli/cli-style.c (style_set_list, style_show_list): Make extern.
> 	* gdbcmd.h (style_set_list, style_show_list): Declare.
> 	* tui/tui-io.c (apply_ansi_escape): Return early if styling the
> 	current position is disabled.
> 	(tui_set_reverse_mode): If reversing, and source styling for the
> 	current position is disabled, switch to default style, reversed.
> 	* tui/tui-win.c (style_tui_current_position)
> 	(show_style_tui_current_position, set_style_tui_current_position):
> 	New.
> 	(_initialize_tui_win): Install the "set/show style
> 	tui-current-position" commands.
> 	* tui/tui-win.h (style_tui_current_position): Declare.
> 
> gdb/doc/ChangeLog:
> 
> 	* gdb.texinfo (Output Styling): Document "set/show style
> 	tui-current-position".
> 	(TUI Overview): Document source code highlighting for the current
> 	position indicator and mention "set style tui-current-position
> 	off".

OK for the documentation parts.

Thanks.