unicode dans coqide

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8475 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 111 insertions, 2 deletions

diff --git a/doc/RefMan-ide.tex b/doc/RefMan-ide.tex
index 148121324..d1497f162 100644
--- a/doc/RefMan-ide.tex
+++ b/doc/RefMan-ide.tex
@@ -178,7 +178,10 @@ contents into files named \verb|#f#| for each opened file
 \verb|f|. You may also activate the \emph{revert} feature: in case a
 opened file is modified on the disk by a third party, \CoqIDE{} may read
 it again for you. Note that in the case you edited that same file, you
-will be prompt to choose to either discard your changes or not.
+will be prompt to choose to either discard your changes or not. The
+\texttt{File charset encoding} choice is described below in
+Section~\ref{sec:coqidecharencoding}
+ 
 
 The \verb|Externals| section allows to customize the external commands
 for compilation, printing, web browsing. In the browser command, you
@@ -209,7 +212,113 @@ Such a default resource file exists in the \Coq{} library, you may
 copy this file into your home directory, and edit it using any text
 editor, \CoqIDE{} itself for example.
 
-  
+\section{Using unicode symbols}
+
+\CoqIDE{} supports unicode character encoding in its text windows,
+consequently a large set of symbols is available for notations.
+
+\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
+$\forall$ and $\exists$, you may define 
+\begin{quote}\tt
+Notation "$\forall$ x : t, P" := \\
+\qquad  (forall x:t, P) (at level 200, x ident).\\
+Notation "$\exists$ x : t, P" := \\
+\qquad  (exists x:t, P) (at level 200, x ident).
+\end{quote}
+There exists a small set of such notations already defined, in the
+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
+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
+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
+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
+symbol required, for example \verb|2200| for the $\forall$ symbol.
+A list of symbol codes is available at \url{http://www.unicode.org}. 
+
+Of course, this method is painful for symbols you use often. There is
+always the possibility to copy-paste a symbol already typed in.
+Another method is to bind some key combinations for frequently used
+symbols. For example, to bind keys \verb|F11| and \verb|F12| to
+$\forall$ and $\exists$ respectively, you may add
+\begin{quote}\tt
+  bind "F11" {"insert-at-cursor" ("$\forall$")}\\
+  bind "F12" {"insert-at-cursor" ("$\exists$")}
+\end{quote}
+to your \verb|binding "text"| section in \verb|.coqiderc-gtk2rc|.
+
+
+%  such a binding is system-dependent. We
+% give here a solution for X11:
+% \begin{itemize}
+% \item first, using \verb|xmodmap|, bind some key combination into a
+%   new key name such as Fxx where xx greater that 12: for example (on a
+%   french keyboard)
+%   \begin{quote}\tt
+%     xmodmap -e "keycode  24 = a A F13 F13" \\
+%     xmodmap -e "keycode  26 = e E F14 F14" 
+%   \end{quote}
+%   will rebind "<AltGr>a" to F13 and "<AltGr>e" to F14.
+% \item then add   
+%   \begin{quote}\tt
+%     bind "F13" {"insert-at-cursor" ("$\forall$")}\\
+%     bind "F14" {"insert-at-cursor" ("$\exists$")}
+%   \end{quote}
+%   to your \verb|binding "text"| section in \verb|.coqiderc-gtk2rc|.
+%        The strange \verb|∀| argument is the UTF-8 encoding for
+%        0x2200, that is the symbol $\forall$. Computing UTF-8 encoding
+%        for a unicode can be done in various ways, including
+%        launching a \verb|lablgtk2| toplevel and use
+%\begin{verbatim}
+%     Glib.Utf8.from_unichar 0x2200;;
+%\end{verbatim}
+%\end{itemize}
+
+\subsection{Character encoding for saved files}
+\label{sec:coqidecharencoding}
+
+In the \texttt{Files} section of the preferences, the encoding option
+is related to the way files are saved. 
+
+If you have no need to exchange files with non UTF-8 aware
+applications, it is better to choose the UTF-8 encoding, since it
+guarantees that your files will be read again without problems. (This
+is because when \CoqIDE{} reads a file, it tries to automatically
+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.
+
+
+\section{Building a custom \CoqIDE{} with user \textsc{ML} code}
+
+You can do this as described in Section~\ref{Coqmktop} for a
+custom coq text toplevel, simply by adding 
+option \verb|-ide| to \verb|coqmktop|, that is something like
+\begin{quote}
+\texttt{coqmktop -ide -byte $m_1$.cmo \ldots{} $m_n$.cmo}
+\end{quote}
+or 
+\begin{quote}
+\texttt{coqmktop -ide -opt $m_1$.cmx \ldots{} $m_n$.cmx}
+\end{quote}
+
+    
+
 % $Id$ 
 
 %%% Local Variables: