diff options
| author | Hugo Herbelin | 2015-09-26 16:31:29 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2015-09-26 16:33:08 +0200 |
| commit | 4b88d774729e0ab7916730e8e6ebedc2033a87f2 (patch) | |
| tree | a91951ae7b9da321b68c20cb0964b96fbd531dea | |
| parent | 5481ff4f6935874ac3798a61f5a2a810006bde37 (diff) | |
Documenting how to support some special unicode characters in coqdoc
(thanks to coq-club, Sep 2015).
| -rw-r--r-- | doc/refman/coqdoc.tex | 9 | ||||
| -rw-r--r-- | tools/coqdoc/output.ml | 7 |
2 files changed, 14 insertions, 2 deletions
diff --git a/doc/refman/coqdoc.tex b/doc/refman/coqdoc.tex index 30467a5e6e..26dbd59e76 100644 --- a/doc/refman/coqdoc.tex +++ b/doc/refman/coqdoc.tex @@ -507,6 +507,15 @@ Default behavior is to assume ASCII 7 bits input files. \texttt{forall}. \LaTeX\ UTF-8 support can be found at \url{http://www.ctan.org/pkg/unicode}. + For the interpretation of Unicode characters by \LaTeX, extra + packages which {\coqdoc} does not provide by default might be + required, such as \texttt{textgreek} for some Greek letters or + \texttt{stmaryrd} for some mathematical symbols. If a Unicode + character is missing an interpretation in the \texttt{utf8x} input + encoding, add + \verb=\DeclareUnicodeCharacter{=\textit{code}\verb=}{=\textit{latex-interpretation}\verb=}=. Packages + and declarations can be added with option \texttt{-p}. + \item[\texttt{\mm{}inputenc} \textit{string}] ~\par Give a \LaTeX\ input encoding, as an option to \LaTeX\ package diff --git a/tools/coqdoc/output.ml b/tools/coqdoc/output.ml index 06030c45a6..8589f94a01 100644 --- a/tools/coqdoc/output.ml +++ b/tools/coqdoc/output.ml @@ -197,8 +197,11 @@ module Latex = struct printf "\n"; printf "%%Warning: tipa declares many non-standard macros used by utf8x to\n"; printf "%%interpret utf8 characters but extra packages might have to be added\n"; - printf "%%(e.g. \"textgreek\" for Greek letters not already in tipa).\n"; - printf "%%Use coqdoc's option -p to add new packages.\n"; + printf "%%such as \"textgreek\" for Greek letters not already in tipa\n"; + printf "%%or \"stmaryrd\" for mathematical symbols.\n"; + printf "%%Utf8 codes missing a LaTeX interpretation can be defined by using\n"; + printf "%%\\DeclareUnicodeCharacter{code}{interpretation}.\n"; + printf "%%Use coqdoc's option -p to add new packages or declarations.\n"; printf "\\usepackage{tipa}\n"; printf "\n" |