Commit 775b5164 authored by MARCHE Claude's avatar MARCHE Claude

a few additions in the doc for GUI

parent 5e2a954e
...@@ -58,7 +58,7 @@ ...@@ -58,7 +58,7 @@
* debuguer cpulimit pour gappa (pb de return code) * debuguer cpulimit pour gappa (pb de return code)
* option -version a tous les executables (TODO: Andrei) * option --version a tous les executables (done, except IDE)
** + affichage dans l'IDE (done) ** + affichage dans l'IDE (done)
* Builtin arrays in provers (done) * Builtin arrays in provers (done)
* make install (done) * make install (done)
......
...@@ -222,11 +222,30 @@ the actions of the various menus and buttons of the interface. ...@@ -222,11 +222,30 @@ the actions of the various menus and buttons of the interface.
\subsection{Menus} \subsection{Menus}
\paragraph{Menu \textsf{File}}
\begin{description} \begin{description}
\item[File/Detect provers] runs provers auto-detection \item[Add File] adds a file in the GUI
\item[File/Preferences] opens a window for modifying preferred configuration \item[Detect provers] runs provers auto-detection
\item[Preferences] opens a window for modifying preferred
configuration, see details below
\item[Quit] exits the GUI
\end{description} \end{description}
\paragraph{Menu \textsf{View}}
\begin{description}
\item[Expand All] expands all the rows of the tree view
\item[Collapse proved goals] closes all the rows of the tree view
which are proved.
\item[Hide proved goals] completely hides the proved rows of the tree
view [EXPERIMENTAL]
\end{description}
\paragraph{Menu \textsf{Tools}}
A copy of the tools already available in the left toolbar
\paragraph{Menu \textsf{Help}}
A very short online help, and some information about this software.
\subsection{Preferences} \subsection{Preferences}
The preferences window allows you customize The preferences window allows you customize
...@@ -340,6 +359,12 @@ Here is a quick documentation of provided transformations. We give ...@@ -340,6 +359,12 @@ Here is a quick documentation of provided transformations. We give
first the non-splitting ones, \eg{} those which produce one goal as first the non-splitting ones, \eg{} those which produce one goal as
result, and others which produces any number of goals. result, and others which produces any number of goals.
Notice that the set of available transformations in your own
installation is given by
\begin{verbatim}
why3 --list-transforms
\end{verbatim}
\subsection{Non-splitting transformations} \subsection{Non-splitting transformations}
\begin{description} \begin{description}
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment