From 5481ff4f6935874ac3798a61f5a2a810006bde37 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sat, 26 Sep 2015 15:00:33 +0200 Subject: Clarifying the doc of coqdoc --utf8 as discussed on coq-club on August 19, 2015. --- doc/refman/coqdoc.tex | 14 ++++++++------ 1 file changed, 8 insertions(+), 6 deletions(-) (limited to 'doc') diff --git a/doc/refman/coqdoc.tex b/doc/refman/coqdoc.tex index ee2b042f4e..30467a5e6e 100644 --- a/doc/refman/coqdoc.tex +++ b/doc/refman/coqdoc.tex @@ -285,7 +285,7 @@ suffix \verb!.tex!. Select a \texmacs\ output. -\item[\texttt{--stdout}] ~\par +\item[\texttt{\mm{}stdout}] ~\par Write output to stdout. @@ -496,14 +496,16 @@ Default behavior is to assume ASCII 7 bits input files. \item[\texttt{-latin1}, \texttt{\mm{}latin1}] ~\par Select ISO-8859-1 input files. It is equivalent to - \texttt{--inputenc latin1 --charset iso-8859-1}. + \texttt{\mm{}inputenc latin1 \mm{}charset iso-8859-1}. \item[\texttt{-utf8}, \texttt{\mm{}utf8}] ~\par - Select UTF-8 (Unicode) input files. It is equivalent to - \texttt{--inputenc utf8 --charset utf-8}. - \LaTeX\ UTF-8 support can be found at - \url{http://www.ctan.org/pkg/unicode}. + Set \texttt{\mm{}inputenc utf8x} for \LaTeX\ output and + \texttt{\mm{}charset utf-8} for HTML output. Also use Unicode + replacements for a couple of standard plain ASCII notations such + as $\rightarrow$ for \texttt{->} and $\forall$ for + \texttt{forall}. \LaTeX\ UTF-8 support can be found at + \url{http://www.ctan.org/pkg/unicode}. \item[\texttt{\mm{}inputenc} \textit{string}] ~\par -- cgit v1.2.3 From 4b88d774729e0ab7916730e8e6ebedc2033a87f2 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sat, 26 Sep 2015 16:31:29 +0200 Subject: Documenting how to support some special unicode characters in coqdoc (thanks to coq-club, Sep 2015). --- doc/refman/coqdoc.tex | 9 +++++++++ 1 file changed, 9 insertions(+) (limited to 'doc') 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 -- cgit v1.2.3 From 2cf609c41f7af83d9eaf43308a368fcb7307e6fa Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Mon, 28 Sep 2015 11:04:59 +0200 Subject: Make -load-vernac-object respect the loadpath. This command-line option was behaving like the old -require, except that it did not do Import. In other words, it was loading files without respecting the loadpath. Now it behaves exactly like Require, while -require now behaves like Require Import. This patch also removes Library.require_library_from_file and all its dependencies, since they are no longer used inside Coq. --- doc/refman/RefMan-com.tex | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'doc') diff --git a/doc/refman/RefMan-com.tex b/doc/refman/RefMan-com.tex index 0f1823a021..9862abb533 100644 --- a/doc/refman/RefMan-com.tex +++ b/doc/refman/RefMan-com.tex @@ -153,9 +153,9 @@ Add physical path {\em directory} to the {\ocaml} loadpath. Load \Coq~file {\em file}{\tt .v} optionally with copy it contents on the standard input. -\item[{\tt -load-vernac-object} {\em file}]\ +\item[{\tt -load-vernac-object} {\em path}]\ - Load \Coq~compiled file {\em file}{\tt .vo} + Load \Coq~compiled library {\em path} (equivalent to {\tt Require} {\em path}). \item[{\tt -require} {\em path}]\ -- cgit v1.2.3 From 9186689cbd5062a2535413369c72896e6f53a69b Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Wed, 30 Sep 2015 15:38:22 +0200 Subject: Fixing documentation wrt the ctrl-shift-u Unicode input method (see #2013). Incidentally made writing style in CoqIDE chapter more homogeneous. --- doc/refman/RefMan-ide.tex | 33 ++++++++++++++++++--------------- 1 file changed, 18 insertions(+), 15 deletions(-) (limited to 'doc') diff --git a/doc/refman/RefMan-ide.tex b/doc/refman/RefMan-ide.tex index c8d05013b3..c6fbd1c538 100644 --- a/doc/refman/RefMan-ide.tex +++ b/doc/refman/RefMan-ide.tex @@ -215,12 +215,13 @@ mouse button, press the key you want for the new shortcut, and release the mouse button afterwards. If your system does not allow it, you may still edit this configuration file by hand, but this is more involved. -\section{Using unicode symbols} +\section{Using Unicode symbols} -\CoqIDE{} supports unicode character encoding in its text windows, -consequently a large set of symbols is available for notations. +\CoqIDE{} is based on GTK+ and inherits from it support for Unicode in +its text windows. Consequently a large set of symbols is available for +notations. -\subsection{Displaying unicode symbols} +\subsection{Displaying Unicode symbols} You just need to define suitable notations as described in Chapter~\ref{Addoc-syntax}. For example, to use the mathematical symbols @@ -236,31 +237,33 @@ file \verb|utf8.v| of \Coq{} library, so you may enable them just by \verb|Require utf8| inside \CoqIDE{}, or equivalently, by starting \CoqIDE{} with \verb|coqide -l utf8|. -However, there are some issues when using such unicode symbols: you of +However, there are some issues when using such Unicode symbols: you of course need to use a character font which supports them. In the Fonts -section of the preferences, the Preview line displays some unicode symbols, so +section of the preferences, the Preview line displays some Unicode symbols, so you could figure out if the selected font is OK. Related to this, one -thing you may need to do is choose whether Gtk should use antialiased +thing you may need to do is choose whether GTK+ should use antialiased fonts or not, by setting the environment variable \verb|GDK_USE_XFT| to 1 or 0 respectively. \subsection{Defining an input method for non ASCII symbols} -To input an Unicode symbol, a general method is to press both the -CONTROL and the SHIFT keys, and type the hexadecimal code of the +To input a Unicode symbol, a general method provided by GTK+ +is to simultaneously press the +Control, Shift and ``u'' keys, release, then type the hexadecimal code of the symbol required, for example \verb|2200| for the $\forall$ symbol. A list of symbol codes is available at \url{http://www.unicode.org}. -This method obviously doesn't scale, that's why the preferred alternative is to -use an Input Method Editor. On POSIX systems (Linux distros, BSD variants and -MacOS X), you can use \texttt{uim} version 1.6 or later which provides a \LaTeX{}-style +An alternative method which does not require to know the hexadecimal +code of the character is to use an Input Method Editor. On POSIX +systems (Linux distributions, BSD variants and MacOS X), you can use +\texttt{uim} version 1.6 or later which provides a \LaTeX{}-style input method. To configure \texttt{uim}, execute \texttt{uim-pref-gtk} as your regular user. In the "Global Settings" group set the default Input Method to "ELatin" (don't forget to tick the checkbox "Specify default IM"). In the "ELatin" group set the layout to "TeX", and remember the content of the "[ELatin] on" field (by default -"\textbackslash"). You can now execute CoqIDE with the following commands (assuming +Control-\textbackslash). You can now execute CoqIDE with the following commands (assuming you use a Bourne-style shell): \begin{verbatim} @@ -268,7 +271,7 @@ $ export GTK_IM_MODULE=uim $ coqide \end{verbatim} -Activate the ELatin Input Method with Ctrl-\textbackslash, then type the +Activate the ELatin Input Method with Control-\textbackslash, then type the sequence "\verb=\Gamma=". You will see the sequence being replaced by $\Gamma$ as soon as you type the second "a". @@ -286,7 +289,7 @@ detect its character encoding.) If you choose something else than UTF-8, then missing characters will be written encoded by \verb|\x{....}| or \verb|\x{........}| where each dot is an hexadecimal digit: the number between braces is the -hexadecimal UNICODE index for the missing character. +hexadecimal Unicode index for the missing character. %%% Local Variables: -- cgit v1.2.3