diff options
author | 2003-12-12 14:15:07 +0000 | |
---|---|---|
committer | 2003-12-12 14:15:07 +0000 | |
commit | e5e298a5f0fedc1a6f884477986e1de8afbb302b (patch) | |
tree | 9a40db534927d73c9a95507fe9e70cfed70f68c9 | |
parent | 9ca885e2637dcb48924403df76f481d637ddd5a0 (diff) |
coqide
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8385 85f007b7-540e-0410-9357-904b9bb8a0f7
-rw-r--r-- | doc/.cvsignore | 1 | ||||
-rw-r--r-- | doc/Makefile | 23 | ||||
-rw-r--r-- | doc/RefMan-ide.tex | 43 | ||||
-rw-r--r-- | doc/coqide-queries.png | bin | 0 -> 27316 bytes |
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 Binary files differnew file mode 100644 index 000000000..dea5626f8 --- /dev/null +++ b/doc/coqide-queries.png |