From 334cbcdffd811135cbc282ef1eace1bc69b0ccbd Mon Sep 17 00:00:00 2001 From: vgross Date: Thu, 7 Oct 2010 15:07:27 +0000 Subject: TeX input method is now supported upstream git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13514 85f007b7-540e-0410-9357-904b9bb8a0f7 --- doc/refman/RefMan-ide.tex | 20 +++++++++++--------- 1 file changed, 11 insertions(+), 9 deletions(-) (limited to 'doc') diff --git a/doc/refman/RefMan-ide.tex b/doc/refman/RefMan-ide.tex index c00a389f46..4b448ad0be 100644 --- a/doc/refman/RefMan-ide.tex +++ b/doc/refman/RefMan-ide.tex @@ -263,22 +263,24 @@ 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} and the CoqIDE IM module to support \LaTeX{}-style -edition. To do this, you must have \texttt{uim} installed on your system. -Then, issue a \texttt{make install-im} as root from the Coq source directory +MacOS X), you can use \texttt{uim} version 1.6 or later which provides a \LaTeX{}-style +input method. -If everything went right, execute \texttt{uim-pref-gtk} as your regular user -and in the "Global Settings" menu set the default Input Method to "CoqIDE" -(don't forget to tick the checkbox "Specify default IM"). You can now execute -CoqIDE with the following commands (assuming you use a Bourne-style shell): +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): \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". +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}} -- cgit v1.2.3