doc: update LaTeX highlighting section

doc/syntax_highlight_in_latex.md

@@ -1,40 +1,12 @@
-We provide a way to syntax-highlight Lean code in LaTeX documents.
-It requires a Python package `Pygments` and a LaTeX package `minted`.
+The [Pygments](https://pygments.org/) syntax highlighting library has official support for Lean (however, Lean 4 keywords have not been added yet), which can be used in LaTeX via the [`minted`](https://ctan.org/pkg/minted) package.
 
+# Example
 
-Python Package: `Pygments`
---------------------------
-
-Checkout [Leanprover's Pygments repository][lean-pygments] and build Pygments:
-
-```bash
-hg clone https://bitbucket.org/leanprover/pygments-main
-cd pygments-main
-make mapfiles
-sudo ./setup.py install
-````
-
-[lean-pygments]: https://bitbucket.org/leanprover/pygments-main
-
-
-LaTeX package: `minted`
------------------------
-
-Save the latest version of [minted.sty][minted.sty] at the working directory.
-
-[minted]: https://github.com/gpoore/minted
-[minted.sty]: https://raw.githubusercontent.com/gpoore/minted/master/source/minted.sty
-
-
-How to use them (example)
--------------------------
-
-Please save the following sample LaTeX file as `test.tex`:
+Save the following sample LaTeX file as `test.tex`:
 
 ```latex
 \documentclass{article}
 \usepackage{minted}
-\setminted{encoding=utf-8}
 \usepackage{fontspec}
 \setmainfont{FreeSerif}
 \setmonofont{FreeMono}
@@ -61,11 +33,13 @@ xelatex --shell-escape test
 
 Some remarks:
 
- - `xelatex` is required to handle unicode in LaTeX.
- - `--shell-escape` option is needed to allow `xelatex` to execute `pygmentize` in a shell.
-
-
-Contribute
-----------
-
-Please fork [Leanprover's Pygments repository][lean-pygments], improve it, and make a pull-request.
+ - either `xelatex` or `lualatex` is required to handle Unicode characters in the code.
+ - `--shell-escape` is needed to allow `xelatex` to execute `pygmentize` in a shell.
+ - If the chosen monospace font is missing some Unicode symbols, you can direct them to be displayed using a fallback font.
+``` latex
+\usepackage{newunicodechar}
+\newfontfamily{\freeserif}{DejaVu Sans}
+\newunicodechar{✝}{\freeserif{✝}}
+```
+ - minted has a "helpful" feature that draws red boxes around characters the chosen lexer doesn't recognize.
+ Since the Lean lexer cannot encompass all user-defined syntax, it is advisable to [work around](https://tex.stackexchange.com/a/343506/14563) this feature.