coqide

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

5 files changed, 106 insertions, 2 deletions

diff --git a/doc/Makefile b/doc/Makefile
index ae057235ab..066d010bbc 100644
--- a/doc/Makefile
+++ b/doc/Makefile
@@ -45,8 +45,8 @@ COQTEXFILES= Cases.v.tex Coercion.v.tex Extraction.v.tex Program.v.tex\
   Correctness.v.tex Setoid.v.tex
 
 REFMANFILES= Reference-Manual.tex RefMan-pre.tex RefMan-int.tex \
-  RefMan-pro.tex RefMan-com.tex RefMan-uti.tex RefMan-add.tex \
-  RefMan-modr.tex \
+  RefMan-pro.tex RefMan-com.tex RefMan-uti.tex RefMan-ide.tex \
+  coqide.eps RefMan-add.tex RefMan-modr.tex \
   $(REFMANCOQTEXFILES) 
 
 REFMAN=Reference-Manual
@@ -90,6 +90,11 @@ all-ps: Tutorial.v.ps Reference-Manual.ps # Library.ps Changes.v.ps
 all-html: Tutorial.v.html Reference-Manual.html # Library.html Changes.v.html
 
 
+#image coqide
+coqide.eps: coqide.png
+	pngtopnm coqide.png | pnmtops -noturn -rle > coqide.eps
+
+
 # dvips et dviselect existent sur loupiac
 distrib:
 	make check-env
diff --git a/doc/RefMan-ide.tex b/doc/RefMan-ide.tex
new file mode 100644
index 0000000000..a415dfb95c
--- /dev/null
+++ b/doc/RefMan-ide.tex
@@ -0,0 +1,90 @@
+\chapter{\Coq{} Integrated Development Environment}
+%\label{Addoc-coqide}
+\ttindex{coqide}
+
+The \Coq{} Integrated Development Environment is a graphical tool, to
+be used as a user-friendly replacement to \texttt{coqtop}. Its main
+purpose is to allow the user to navigate forward and backward into a
+\Coq{} vernacular file, executing corresponding commands or undoing
+them respectively. CREDITS ? Proof general, lablgtk, ...
+
+\coqide{} is run by typing the command \verb|coqide| on the command
+line. Without argument, the main screen is displayed with an ``unnamed
+buffer'', and with a file name as argument, another buffer displaying
+the contents of that file. Additionally, coqide accepts the same
+options as coqtop, given in Chapter~\ref{Addoc-coqc}, the ones having
+obviously no meaning for \coqide{} being ignored.
+
+\begin{figure}[t]
+\begin{center}
+\ifx\pdftexversion\undefined   % si on est pas en pdflatex
+\includegraphics[width=1.0\textwidth]{coqide.eps}
+\else
+\includegraphics[width=1.0\textwidth]{coqide.png}
+\fi
+\end{center}
+\caption{Coqide main screen}
+\label{fig:coqide}
+\end{figure}
+
+\coqide{} main screen is shown on Figure~\ref{fig:coqide}.  (Attention
+il manque la toolbar sur cet ecran car je l'ai enleve par defaut) At
+the top is a menu bar, the left window is displaying the various
+buffers, the upper right window is the ``goal window'', where goals to
+prove are displayed. The lower right window is the ``message window'',
+where various messages resulting from commands are displayed. At the
+bottom is the status bar.
+
+\section{The \texttt{File} menu}
+
+Open/Create
+
+Save
+
+Save as
+
+Save all
+
+Revert All Buffers
+
+Close Buffer
+
+Print
+
+Export to
+
+Rehighlight
+
+Quit
+
+\section{The \texttt{Edit} menu}
+
+
+\section{The \texttt{Navigation} menu}
+
+Remplacer forward to et backward to par goto ?
+idem pour la toolbar
+
+\section{The \texttt{Try Tactics} menu}
+
+Is it useful ?
+
+\section{The \texttt{Templates} menu}
+
+Need update to V8 syntax
+
+\section{The \texttt{Commands} menu}
+
+\section{The \texttt{Externals} menu}
+
+\section{The \texttt{Configuration} menu}
+
+\section{The \texttt{Help} menu}
+
+
+% $Id$ 
+
+%%% Local Variables: 
+%%% mode: latex
+%%% TeX-master: "Reference-Manual"
+%%% End: 
diff --git a/doc/Reference-Manual.tex b/doc/Reference-Manual.tex
index af404d505c..01dece65de 100644
--- a/doc/Reference-Manual.tex
+++ b/doc/Reference-Manual.tex
@@ -5,6 +5,13 @@
 \usepackage{verbatim}
 \usepackage{palatino}
 \usepackage{url}
+% for coqide
+\ifx\pdftexversion\undefined   % si on est pas en pdflatex
+  \usepackage[dvips]{graphicx}
+\else
+  \usepackage[pdftex]{graphicx}
+\fi
+
 
 \makeatletter
 
@@ -51,6 +58,7 @@
 \part{Practical tools}
 \include{RefMan-com}% The coq commands (coqc coqtop)
 \include{RefMan-uti}% utilities (gallina, do_Makefile, etc)
+\include{RefMan-ide}% Coq IDE
 
 \include{AddRefMan-pre}%
 \include{Cases.v}%
diff --git a/doc/coqide.png b/doc/coqide.png
new file mode 100644
index 0000000000..d2f1e5d9bc
--- /dev/null
+++ b/doc/coqide.png
diff --git a/doc/macros.tex b/doc/macros.tex
index 2bcffd3543..5c22e72a9a 100755
--- a/doc/macros.tex
+++ b/doc/macros.tex
@@ -65,6 +65,7 @@
 %%%%%%%%%%%%%%%%%%%%%%%%
 
 \newcommand{\Coq}{{\sf Coq}}
+\newcommand{\coqide}{\textsc{CoqIDE}}
 \newcommand{\ocaml}{{\sf Objective Caml}}
 \newcommand{\camlpppp}{{\sf Camlp4}}
 \newcommand{\emacs}{{\sf GNU Emacs}}