Commit 1eb33ff3 authored by MARCHE Claude's avatar MARCHE Claude

why3 session update -rename-file: documentation and CHANGES updated

parent d55ea9b9
...@@ -9,6 +9,12 @@ Transformations ...@@ -9,6 +9,12 @@ Transformations
* "destruct_rec" applies "destruct" recursively on a goal (issue 231). * "destruct_rec" applies "destruct" recursively on a goal (issue 231).
* "destruct" now simplifies away equalities on constructors. * "destruct" now simplifies away equalities on constructors.
Tools
* add a command 'why3 session update' to modify sessions from the
command line. So far, only one option exists, for renaming files
fixes issue #227
Version 1.1.0, October 17, 2018 Version 1.1.0, October 17, 2018
------------------------------- -------------------------------
......
...@@ -698,15 +698,14 @@ The available subcommands are as follows: ...@@ -698,15 +698,14 @@ The available subcommands are as follows:
\item[\texttt{info}] prints informations and statistics about sessions. \item[\texttt{info}] prints informations and statistics about sessions.
\item[\texttt{latex}] outputs session contents in LaTeX format. \item[\texttt{latex}] outputs session contents in LaTeX format.
\item[\texttt{html}] outputs session contents in HTML format. \item[\texttt{html}] outputs session contents in HTML format.
\item[\texttt{mod}] modifies some of the proofs, selected by a filter. \item[\texttt{update}] update session contents.
\item[\texttt{copy}] duplicates some of the proofs, selected by a filter. %\item[\texttt{mod}] modifies some of the proofs, selected by a filter.
\item[\texttt{rm}] removes some of the proofs, selected by a filter. %\item[\texttt{copy}] duplicates some of the proofs, selected by a filter.
%\item[\texttt{rm}] removes some of the proofs, selected by a filter.
\end{description} \end{description}
The first three commands do not modify the sessions, whereas the last The first three commands do not modify the sessions, whereas the last
four modify them. Only the proof attempts recorded are modified. No modify them.
prover is called on the modified or created proof attempts, and
consequently the proof status is always marked as obsolete.
\subsection{Command \texttt{info}} \subsection{Command \texttt{info}}
...@@ -974,6 +973,16 @@ Specific options for this command are as follows. ...@@ -974,6 +973,16 @@ Specific options for this command are as follows.
\end{description} \end{description}
\subsection{Command \texttt{update}}
The command \texttt{why3 session update} permits to modify
the session contents, depending on the following specific options.
\begin{description}
\item[\texttt{-rename-file \textsl{<src>} \textsl{<dst>}}] renames the file \textsl{<src>} to \textsl{<dst>} in the session. The file \textsl{<src>} itself is also renamed to \textsl{<dst>} in your filesystem.
\end{description}
\section{The \texttt{doc} Command} \section{The \texttt{doc} Command}
\label{sec:why3doc} \label{sec:why3doc}
......
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