coqide

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

4 files changed, 50 insertions, 17 deletions

diff --git a/doc/.cvsignore b/doc/.cvsignore
index a6109f3d0..b56727b62 100644
--- a/doc/.cvsignore
+++ b/doc/.cvsignore
@@ -36,3 +36,4 @@ library.files.ls.tmp
 library.coqweb.tex
 tradv8
 coqide.eps
+coqide-queries.eps
diff --git a/doc/Makefile b/doc/Makefile
index aac7fbda8..a6f561093 100644
--- a/doc/Makefile
+++ b/doc/Makefile
@@ -17,7 +17,7 @@
 DOCCOQTOP=$(COQBIN)/coqtop #.byte
 DOCCOQC=$(COQBIN)/coqc
 COQTOP=`$(DOCCOQC) -where`
-COQTEX=$(COQBIN)/coq-tex -image $(DOCCOQTOP) -v -sl -small
+COQTEX=$(COQBIN)/coq-tex -n 72 -image $(DOCCOQTOP) -v -sl -small
 #COQWEBSTY=$(HOME)/lib/tex/
 COQWEBSTY=/usr/share/texmf/tex/latex/misc/
 HEVEALIB=/usr/local/lib/hevea
@@ -48,7 +48,7 @@ COQTEXFILES= Cases.v.tex Coercion.v.tex Extraction.v.tex Program.v.tex\
 
 REFMANFILES= Reference-Manual.tex RefMan-pre.tex RefMan-int.tex \
   RefMan-pro.tex RefMan-com.tex RefMan-uti.tex RefMan-ide.tex \
-  coqide.eps RefMan-add.tex RefMan-modr.tex \
+  coqide.eps coqide-queries.eps RefMan-add.tex RefMan-modr.tex \
   $(REFMANCOQTEXFILES) 
 
 REFMAN=Reference-Manual
@@ -95,10 +95,6 @@ all-html: Tutorial.v.html Reference-Manual.html # Library.html Changes.v.html
 version.tex: Makefile
 	echo "\newcommand{\coqversion}{$(VERSION)}" > version.tex
 
-#image coqide
-coqide.eps: coqide.png
-	pngtopnm coqide.png | pnmtops -equalpixels -noturn -rle > coqide.eps
-
 
 # dvips et dviselect existent sur loupiac
 distrib:
@@ -202,7 +198,7 @@ cleanall: clean clean-html
 # Implicit rules
 #########################
 
-.SUFFIXES: .dvi .tex .v.tex .ps .pdf
+.SUFFIXES: .dvi .tex .v.tex .ps .pdf .eps .png
 
 .tex.dvi:
 	$(LATEX) $<
@@ -218,6 +214,10 @@ cleanall: clean clean-html
 .dvi.ps:
 	dvips -o $@ $<
 
+%.eps: %.png
+	pngtopnm $< | pnmtops -equalpixels -noturn -rle > $@
+
+
 
 ##########################
 # Dependencies
@@ -290,22 +290,13 @@ Tutorial.v.pdf: ./title.tex Tutorial.v.tex
 Reference-Manual.ps: Reference-Manual.dvi
 
 Reference-Manual.dvi: $(INPUTS) $(REFMANFILES) $(COQTEXFILES) biblio.bib
-	#rm -f Reference-Manual.sh
 	$(LATEX) Reference-Manual
-	#rm Reference-Manual.sh
 	$(BIBTEX) Reference-Manual
-	$(LATEX) Reference-Manual
-	#rm Reference-Manual.sh
-	$(BIBTEX) Reference-Manual
-	$(LATEX) Reference-Manual
-	#rm Reference-Manual.sh
 	$(MAKEINDEX) Reference-Manual
 	$(MAKEINDEX) Reference-Manual.tacidx -o Reference-Manual.tacind
 	$(MAKEINDEX) Reference-Manual.comidx -o Reference-Manual.comind
 	$(MAKEINDEX) Reference-Manual.erridx -o Reference-Manual.errind
 	$(LATEX) Reference-Manual
-	#rm Reference-Manual.sh
-	$(LATEX) Reference-Manual
 
 Reference-Manual.pdf: Reference-Manual.dvi
 	#rm -f Reference-Manual.sh
diff --git a/doc/RefMan-ide.tex b/doc/RefMan-ide.tex
index 5fa42d571..c38388c54 100644
--- a/doc/RefMan-ide.tex
+++ b/doc/RefMan-ide.tex
@@ -105,9 +105,50 @@ arguments.
 
 \section{Queries}
 
+\begin{figure}[t]
+\begin{center}
+%HEVEA\imgsrc{coqide-queries.png}
+%BEGIN LATEX
+\ifx\pdfoutput\undefined   % si on est pas en pdflatex
+\includegraphics[width=1.0\textwidth]{coqide-queries.eps}
+\else
+\includegraphics[width=1.0\textwidth]{coqide-queries.png}
+\fi
+%END LATEX
+\end{center}
+\caption{Coqide main screen}
+\label{fig:querywindow}
+\end{figure}
+
+
+We call \emph{query} any vernacular command that do not change the
+current state, such as \verb|Check|, \verb|SearchAbout|, etc. Those
+commands are of course useless during compilation of a file, hence
+should not be included in scripts. To run such commands without
+writing them in the script, \coqide{} offers another input window
+called the \emph{query window}. This window can be displayed on
+demand, either by using the \texttt{Window} menu, or directly using
+shortcuts given in the \texttt{Queries} menu. Indeed, with \coqide{}
+the simplest way to perform a \texttt{SearchAbout} on some identifier
+is to select it using the mouse, and pressing \verb|F2|. This will
+both make appear the query window ans run the \texttt{SearchAbout} in
+it, displaying the result. Shortcuts \verb|F3| and \verb|F4| are for
+\verb|Check| and \verb|Print| respectively.
+Figure~\ref{fig:querywindow} displays the query window after selection
+of the word ``mult'' in the script windows, and pressing \verb|F4| to
+print its definition.
+
 \section{Compilation}
 
-\section{Preferences}
+The \verb|Compile| menu offers direct commands to compile the current
+buffer, compile a set of files using \verb|make|, and creating a
+\verb|makefile| using \verb|coq_makefile|.
+
+TODO: \verb|Next error| !
+
+\section{Customizations}
+
+Menu \texttt{Edit/Preferences}.
 
 auto save, auto revert, delays
 
diff --git a/doc/coqide-queries.png b/doc/coqide-queries.png
new file mode 100644
index 000000000..dea5626f8
--- /dev/null
+++ b/doc/coqide-queries.png