diff options
author | 2004-01-14 15:00:36 +0000 | |
---|---|---|
committer | 2004-01-14 15:00:36 +0000 | |
commit | 4ba765fe88d88e5765d6058b7d366e03318b789a (patch) | |
tree | b134d93f0d9c3771822f8154b24ea219871ec485 | |
parent | 5105f47b13a2b6978abe8bf390709c7d8a61e4a9 (diff) |
unicode dans coqide
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8475 85f007b7-540e-0410-9357-904b9bb8a0f7
-rw-r--r-- | doc/RefMan-ide.tex | 113 |
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: |