Documenting use of colors in Coq.

2 files changed, 16 insertions, 0 deletions

diff --git a/CHANGES b/CHANGES
index f75085a83c..a63b92ae7a 100644
--- a/CHANGES
+++ b/CHANGES
@@ -271,6 +271,9 @@ Interfaces
 - CoqIDE uses the new STM machinery, allowing for asynchronous edition.
 - CoqIDE highlight in yellow "unsafe" commands such as axiom
   declarations, and tactics like "admit".
+- Coqtop outputs highlighted syntax. Colors can be configured thanks
+  to the COQ_COLORS environment variable, and their current state can
+  be displayed with the -list-tags command line option.
 
 Internal Infrastructure
 
diff --git a/doc/refman/RefMan-com.tex b/doc/refman/RefMan-com.tex
index 8d128e6b47..774ba0ed54 100644
--- a/doc/refman/RefMan-com.tex
+++ b/doc/refman/RefMan-com.tex
@@ -77,6 +77,14 @@ look for the commands in directory specified by \verb:$COQBIN:. If
 this variable is not set, they look for the command in the executable
 path.
 
+The \verb:$COQ_COLORS: environment variable can be used to specify the set of
+colors used by {\tt coqtop} to highlight its output. It uses the same syntax as
+the \verb:$LS_COLORS: variable from GNU's {\tt ls}, that is, a colon-separated
+list of assignments of the form \verb:name=attr1;...;attrn: where {\tt name} is
+the name of the corresponding highlight tag and {\tt attri} is an ANSI escape
+code. The list of highlight tags can be retrieved with the {\tt -list-tags}
+command-line option of {\tt coqtop}.
+
 \subsection{By command line options\index{Options of the command line}
 \label{vmoption}
 \label{coqoptions}}
@@ -235,6 +243,11 @@ Add physical path {\em directory} to the {\ocaml} loadpath.
 
   Print the \Coq's version and exit.
 
+\item[{\tt -list-tags}]\
+
+  Print the highlight tags known by \Coq as well as their currently associated
+  color.
+
 \item[{\tt -h}, {\tt --help}]\ 
 
   Print a short usage and exit.