From 6b691bbd2101fd39395c0d2135fd7c06a8915e14 Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Fri, 24 Dec 2010 11:53:29 +0100 Subject: Imported Upstream version 8.3pl1 --- doc/refman/RefMan-ide.tex | 36 +++++++++++++++++++++--------------- 1 file changed, 21 insertions(+), 15 deletions(-) (limited to 'doc/refman/RefMan-ide.tex') diff --git a/doc/refman/RefMan-ide.tex b/doc/refman/RefMan-ide.tex index 04830531..5d9c8c16 100644 --- a/doc/refman/RefMan-ide.tex +++ b/doc/refman/RefMan-ide.tex @@ -261,26 +261,32 @@ 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 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 -"\"). 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 +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): \begin{verbatim} $ export GTK_IM_MODULE=uim $ coqide \end{verbatim} -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". +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 "$\backslash$"). Proceed then as above. \subsection[Character encoding for saved files]{Character encoding for saved files\label{sec:coqidecharencoding}} @@ -314,7 +320,7 @@ or -% $Id: RefMan-ide.tex 13477 2010-09-30 16:50:00Z vgross $ +% $Id: RefMan-ide.tex 13701 2010-12-10 07:48:30Z herbelin $ %%% Local Variables: %%% mode: latex -- cgit v1.2.3