merge fa coqide

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

1 files changed, 87 insertions, 1 deletions

diff --git a/doc/newfaq/main.tex b/doc/newfaq/main.tex
index cd911842eb..8f6b34942c 100644
--- a/doc/newfaq/main.tex
+++ b/doc/newfaq/main.tex
@@ -1009,12 +1009,98 @@ You can use {\tt coqdoc}.
 
 You can use {\tt coq\_tex}.
 
-\section{CoqIde}
+\section{\CoqIde}
 
 \Question{What is \CoqIde ?}
 
 \CoqIde is a gtk based gui for \Coq.
 
+\Question{How to enable Emacs keybindings ?}
+ Insert \texttt{gtk-key-theme-name = "Emacs"}
+    in your \texttt{.coqide-gtk2rc} file. It may be in the current dir
+    or in \verb#$HOME# dir. This is done by default.
+
+\Question{How to enable antialiased fonts ?}
+
+ Set the \verb#GDK_USE_XFT# variable to \verb#1#. This is by default with \verb#Gtk >= 2.2#.
+    If some of your fonts are not available, set \verb#GDK_USE_XFT# to \verb#0#.
+
+\Question{How to use those Forall and Exists pretty symbols ?}
+ Thanks to the notation features in \Coq, you just need to insert these
+lines in your \Coq buffer :
+\begin{verbatim}
+======================================================================
+Notation "∀ x : t, P" := (forall x:t, P) (at level 200, x ident).
+Notation "∃ x : t, P" := (exists x:t, P) (at level 200, x ident).
+======================================================================
+\end{verbatim}
+Copy/Paste of these lines from this file will not work outside of \CoqIde.
+You need to load a file containing these lines or to enter the "∀" 
+using an input method (see \ref{inputmeth}). To try it just use \verb#Require utf8# from inside
+\CoqIde. 
+To enable these notations automatically start coqide with
+\begin{verbatim}
+	coqide -l utf8
+\end{verbatim}
+In the ide subdir of \Coq library, you will find a sample utf8.v with some 
+pretty simple notations.
+
+\Question{How to define an input method for non ASCII symbols ?}\label{inputmeth}
+
+\begin{itemize}
+\item First solution : type \verb#<CONTROL><SHIFT>2200# to enter a forall in the script widow. 
+	2200 is the hexadecimal code for forall in unicode charts and is encoded as "∀"	
+	in UTF-8.
+	2203 is for exists. See \url{http://www.unicode.org} for more codes.
+\item Second solution : rebind \verb#<AltGr>a# to forall and \verb#<AltGr>e# to exists. 
+	Under X11, you need to use something like
+\begin{verbatim}
+		xmodmap -e "keycode  24 = a A F13 F13" 
+		xmodmap -e "keycode  26 = e E F14 F14"
+\end{verbatim}
+	and then to add   
+\begin{verbatim}
+		bind "F13" {"insert-at-cursor" ("∀")}
+		bind "F14" {"insert-at-cursor" ("∃")}
+\end{verbatim}
+	to your "binding "text"" section in \verb#.coqiderc-gtk2rc.#
+	The strange ("∀") argument is the UTF-8 encoding for
+	0x2200. 
+	You can compute these encodings using the lablgtk2 toplevel with 
+\begin{verbatim}		
+Glib.Utf8.from_unichar 0x2200;;
+\end{verbatim}
+	Further symbols can be bound on higher Fxx keys or on even on other keys you
+	do not need .
+\end{itemize}
+
+\Question{How to build a custom \CoqIde with user ml code ?}
+ Use 
+	coqmktop -ide -byte m1.cmo...mi.cmo
+    or 
+	coqmktop -ide -opt m1.cmx...mi.cmx
+
+\Question{How to customize the shortcuts for menus ?}
+ Two solutions are offered:
+\begin{itemize}
+\item Edit \$HOME/.coqide.keys by hand or
+\item Add "gtk-can-change-accels = 1" in your .coqide-gtk2rc file. Then
+    from \CoqIde, you may select a menu entry and press the desired 
+    shortcut. 
+\end{itemize}
+
+\Question{What encoding should I use? What is this x{iiii} in my file?}
+ The encoding option is related to the way files are saved. 
+ Keep it as UTF-8 until it becomes important for you to exchange files 
+ with non UTF-8 aware applications.
+ If you choose something else than UTF-8, then missing characters will 
+ be encoded by \\x{....} or \\x{........} where each dot is an hex. digit. 
+ The number between braces is the hexadecimal UNICODE index for the
+  missing character.
+    
+
+
+
 \section{Extraction}
 
 \Question{What is program extraction ?}