diff options
Diffstat (limited to 'doc/refman/RefMan-ide.tex')
| -rw-r--r-- | doc/refman/RefMan-ide.tex | 51 |
1 files changed, 14 insertions, 37 deletions
diff --git a/doc/refman/RefMan-ide.tex b/doc/refman/RefMan-ide.tex index 5d9c8c16..f061ef18 100644 --- a/doc/refman/RefMan-ide.tex +++ b/doc/refman/RefMan-ide.tex @@ -261,32 +261,26 @@ 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}. -This method obviously doesn't scale, that's why the preferred -alternative is to use an Input Method Editor. On POSIX systems (Linux -distributions, BSD variants and MacOS X), you can use \texttt{uim} to -support \LaTeX{}-style edition and, if using X Windows, you can also use -the XCompose method (XIM). How to use \texttt{uim} is documented below. - -If you have \texttt{uim} 1.5.x, first manually copy the files located -in directory {\tt ide/uim} of the Coq source distribution to the -{\tt uim} directory of input methods which typically is {\tt - /usr/share/uim}. Execute {\tt uim-module-manager -{-}register - coqide}. Then, execute \texttt{uim-pref-gtk} as regular user and set -the default Input Method to "CoqIDE" in the "Global Settings" group -(don't forget to tick the checkbox "Specify default IM"; you may also -have to first edit the set of "Enabled input method" to add CoqIDE to -the set). You can now execute CoqIDE with the following commands -(assuming you use a Bourne-style shell): +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 +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 +"<Control>\textbackslash"). You can now execute CoqIDE with the following commands (assuming +you use a Bourne-style shell): \begin{verbatim} $ export GTK_IM_MODULE=uim $ coqide \end{verbatim} -If you then type the sequence "\verb=\Gamma=", you will see the sequence being -replaced by $\Gamma$ as soon as you type the second "a". - -If you have \texttt{uim} 1.6.x, the \LaTeX{} input method is built-in. You just have to execute \texttt{uim-pref-gtk} and choose "ELatin" as default Input Method in the "Global Settings". Then, in the "ELatin" group set the layout to "TeX", and remember the content of the "[ELatin] on" field (by default "<Control>$\backslash$"). Proceed then as above. +Activate the ELatin Input Method with Ctrl-\textbackslash, then type the +sequence "\verb=\Gamma=". You will see the sequence being +replaced by $\Gamma$ as soon as you type the second "a". \subsection[Character encoding for saved files]{Character encoding for saved files\label{sec:coqidecharencoding}} @@ -305,23 +299,6 @@ 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: RefMan-ide.tex 13701 2010-12-10 07:48:30Z herbelin $ - %%% Local Variables: %%% mode: latex %%% TeX-master: "Reference-Manual" |