Commit 362c5cb9 authored by MARCHE Claude's avatar MARCHE Claude

finished update of the manpage of IDE

updated DTD
parent 2f77eaa9
......@@ -64,9 +64,10 @@
* choose a logo -> done ?
* complete doc/api.tex: explain how to build theories, apply
transformations, write new functions on terms (A)
* DOC:
** complete api.tex: explain how to build theories, apply
transformations, write new functions on terms (A)
** complete manpages.tex: section "Drivers of external provers" (A+F)
=== Roadmap for third release 0.70, july 2011 ========================
......@@ -92,18 +93,19 @@
* distribute bench files (A + F)
* document new IDE features (C)
* document "Make obsolete" (A)
* Distribution of examples: we should distribute those who have an xml file
under git, and distribute the XML and Coq proofs
(JC)
* (done) update doc for why3replayer
- not done: parler des examples distribues ci dessus
* (partially done) update IDE section of starting.tex (C)
- not done: Replay, clean et remove
* (partially done) update doc for why3replayer
- not done: parler des examples distribues ci dessus
* update IDE section of starting.tex (C)
* DONE document new IDE features (C)
* DONE doc: citer l'article Boogie 2011 quelque part
......
......@@ -268,9 +268,9 @@ the actions of the various menus and buttons of the interface.
\item[Add File] adds a file in the GUI
%\item[Detect provers] runs provers auto-detection
\item[Preferences] opens a window for modifying preferred
configuration, see details below
\item[Reload] \todo{}
\item[Save session] \todo{}
configuration parameters, see details below
\item[Reload] reloads the input files from disk, and update the session state accordingly
\item[Save session] Save current session state on disk. The policy to decide when to save the session is configurable, as described in the preferences below.
\item[Quit] exits the GUI
\end{description}
......@@ -298,12 +298,23 @@ The preferences window allows you customize
to do that for the moment is to manually edit the config file)
\item the time limit given to provers, in seconds
\item the maximal number of simultaneous provers allowed to run in parallel.
\item The policy for saving session \todo{}
\item The policy for saving session:
\begin{itemize}
\item always save on exit (default): the current state of the proof session is saving on exit
\item never save on exit: the current state of the session is never save automatically, you must use menu \textsf{File/Save session} to save when wanted
\item ask whether to save: on exit, a popup window ask whether you
want to save or not.
\end{itemize}
\end{itemize}
\subsection{Structure of the database file}
\todo{[TO BE COMPLETED LATER]}
The session state is stored in an XML file named
\texttt{\textsl{<dir>}/why3session.xml}, where \texttt{\textsl{<dir>}}
is the directory of the project.
The XML file follows the DTD given in \texttt{share/why3session.dtd} and reproduced below.
\verbatiminput{../share/why3session.dtd}
\section{The \texttt{why3ml} tool}
......
<!ELEMENT why3session (file*)>
<!ATTLIST why3session name CDATA #REQUIRED>
<!ELEMENT file (theory*)>
<!ATTLIST file name CDATA #REQUIRED>
<!ATTLIST file verified CDATA #REQUIRED>
<!ATTLIST file expanded CDATA #IMPLIED>
<!ELEMENT theory (goal*)>
<!ATTLIST theory name CDATA #REQUIRED>
<!ATTLIST theory verified CDATA #REQUIRED>
<!ATTLIST theory expanded CDATA #IMPLIED>
<!ELEMENT goal (proof*, transf*)>
<!ATTLIST goal name CDATA #REQUIRED>
<!ATTLIST goal expl CDATA #IMPLIED>
<!ATTLIST goal proved CDATA #REQUIRED>
<!ATTLIST goal sum CDATA #REQUIRED>
<!ATTLIST goal expanded CDATA #IMPLIED>
<!ELEMENT proof (result)>
<!ELEMENT proof (result|undone)>
<!ATTLIST proof prover CDATA #REQUIRED>
<!ATTLIST proof timelimit CDATA #REQUIRED>
<!ATTLIST proof edited CDATA #IMPLIED>
<!ATTLIST proof obsolete CDATA #IMPLIED>
<!ELEMENT result EMPTY>
<!ATTLIST result status (valid|invalid|unknown|timeout|failure) #REQUIRED>
<!ATTLIST result time CDATA #IMPLIED>
<!ELEMENT undone EMPTY>
<!ELEMENT transf (goal*)>
<!ATTLIST transf name CDATA #REQUIRED>
<!ATTLIST transf proved CDATA #REQUIRED>
<!ATTLIST transf expanded CDATA #IMPLIED>
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