diff --git a/doc/gui-0-70-5.png b/doc/gui-0-70-5.png
deleted file mode 100644
index dcbbadd6b04355d8f283d2ddcf99847acc7de5d1..0000000000000000000000000000000000000000
Binary files a/doc/gui-0-70-5.png and /dev/null differ
diff --git a/doc/gui-2.png b/doc/gui-2.png
index 3cba3b54558255afeca6be7cd7c93d7be80ad110..eb61afe7fec366d8004e9113f58c76ce0a864fc3 100644
Binary files a/doc/gui-2.png and b/doc/gui-2.png differ
diff --git a/doc/gui-3.png b/doc/gui-3.png
index d6600a313e09cc0ec659d7eae859568984c7a0b3..9a8740fba0b19e4896a2c5934cbab3d11d9a7a98 100644
Binary files a/doc/gui-3.png and b/doc/gui-3.png differ
diff --git a/doc/gui-4.png b/doc/gui-4.png
index 0dd90c5a47ff64adbc64f57bbdbcf8d31e66dbef..31e877faea67016ef244090593b26391ab544a33 100644
Binary files a/doc/gui-4.png and b/doc/gui-4.png differ
diff --git a/doc/gui-5.png b/doc/gui-5.png
new file mode 100644
index 0000000000000000000000000000000000000000..587a5febc5c3669c21e1347c2b621da67307f123
Binary files /dev/null and b/doc/gui-5.png differ
diff --git a/doc/starting.tex b/doc/starting.tex
index a2573edce591764c254217ab377ba5c841a349ed..fdafa211f990598a86a2f44971b154085b7cb08b 100644
--- a/doc/starting.tex
+++ b/doc/starting.tex
@@ -25,6 +25,7 @@ we show how this file is handled in the \why GUI
 (Section~\ref{sec:gui}) then in batch mode using the \texttt{why3}
 executable (Section~\ref{sec:batch}).
 
+%EXECUTE rm -rf doc/hello_proof/
 %EXECUTE cp examples/logic/hello_proof.why doc/
 
 \section{Getting Started with the GUI}
@@ -35,7 +36,7 @@ files, and check the validity of goals with external provers, in a
 friendly way. This section presents the basic use of this GUI. Please
 refer to Section~\ref{sec:ideref} for a more complete description.
 
-%EXECUTE bin/why3 ide --batch "wait 1;snap doc/gui-1.png" doc/hello_proof.why
+%EXECUTE bin/why3 ide --batch "snap doc/gui-1.png" doc/hello_proof.why
 \begin{figure}[tbp]
 %HEVEA\centering
   \includegraphics[width=\textwidth]{gui-1.png}
@@ -72,7 +73,7 @@ allows to browse inside the theories.
 In this tree view, we have a structured view of the file: this file
 contains one theory, itself containing three goals.
 
-%EXECUTE bin/why3 ide --batch "type next;wait 1;snap doc/gui-2.png" doc/hello_proof.why
+%EXECUTE bin/why3 ide --batch "type next;snap -crop 1024x384+0+0 doc/gui-2.png" doc/hello_proof.why
 \begin{figure}[tbp]
 %HEVEA\centering
  \includegraphics[width=\textwidth]{gui-2.png}
@@ -96,7 +97,7 @@ or the parent file. Let us now select the theory ``HelloProof'' and
 click on the \textsf{Simplify} button. After a short time, you should
 get the display of Figure~\ref{fig:gui3}.
 
-%EXECUTE bin/why3 ide --batch "type alt-ergo;view source;wait 5;snap doc/gui-3.png" doc/hello_proof.why
+%EXECUTE bin/why3 ide --batch "type alt-ergo;view source;wait 3;snap -crop 1024x384+0+0 doc/gui-3.png" doc/hello_proof.why
 \begin{figure}[tbp]
 %HEVEA\centering
 \includegraphics[width=\textwidth]{gui-3.png}
@@ -123,7 +124,7 @@ have two subgoals, and you can try again a prover on them, for example
 Simplify. We already have a lot of goals and proof attempts, so it is a good idea to close the sub-trees which are already proved: this can be done by the menu \textsf{View/Collapse proved goals}, or even better by its shortcut ``Ctrl-C''.
 You should see now what is displayed on Figure~\ref{fig:gui4}.
 
-%EXECUTE bin/why3 ide --batch "type alt-ergo;wait 5;type next;wait 1;type split_goal_wp;wait 2;snap doc/gui-4.png" doc/hello_proof.why
+%EXECUTE bin/why3 ide --batch "type alt-ergo;wait 3;type next;type split_goal_wp;wait 1;snap -crop 1024x384+0+0 doc/gui-4.png;save;wait 1" doc/hello_proof.why
 \begin{figure}[tbp]
 %HEVEA\centering
  \includegraphics[width=\textwidth]{gui-4.png}
@@ -167,9 +168,12 @@ false, \eg
 \end{whycode}
 We can reload the modified file in the IDE using menu \textsf{File/Reload}, or the shortcut ``Ctrl-R''. We get the tree view shown on Figure~\ref{fig:gui5}.
 
+%EXECUTE bin/why3 ide --batch "type next;type coq;wait 1;save;wait 1" doc/hello_proof.why
+%EXECUTE sed -i -e 's/true -> false/false -> false/' doc/hello_proof.why
+%EXECUTE bin/why3 ide --batch "type next;type expand;snap -crop 1024x384+0+0 doc/gui-5.png" doc/hello_proof.why
 \begin{figure}[tbp]
 %HEVEA\centering
-  \includegraphics[width=\textwidth]{gui-0-70-5.png}
+  \includegraphics[width=\textwidth]{gui-5.png}
   \caption{File reloaded after modifying goal $G_2$}
   \label{fig:gui5}
 \end{figure}
@@ -305,7 +309,7 @@ hello_proof.why HelloProof G2 : Valid (0.00s)
 Section~\ref{sec:transformations} gives the description of the various
 transformations available.
 
-%EXECUTE rm doc/hello_proof.why
+%EXECUTE rm -r doc/hello_proof.why doc/hello_proof/
 
 %%% Local Variables:
 %%% mode: latex
diff --git a/doc/why3ide-doc.conf b/doc/why3ide-doc.conf
index 610e023fa37b1f23f391ced1f5692a5457051aa2..e5aa9db4acd1aa5b07bc663e579b7b521fe835f7 100644
--- a/doc/why3ide-doc.conf
+++ b/doc/why3ide-doc.conf
@@ -1,5 +1,5 @@
 [editor coqide]
-command = "coqide -I %l/coq-tactic -R %l/coq-tactic Why3 -R %l/coq Why3 %f"
+command = "true %f"
 name = "CoqIDE"
 
 [ide]
diff --git a/src/ide/why3ide.ml b/src/ide/why3ide.ml
index a14b405c6bad56fc57328a3761b31227ad7967b2..6b58c402d959cf1e52613590daeebea62dfe2f19 100644
--- a/src/ide/why3ide.ml
+++ b/src/ide/why3ide.ml
@@ -2340,7 +2340,7 @@ let batch s =
   let last = ref (Sys.time ()) in
   fun () ->
   let t = Sys.time () in
-  if not !initialization_complete || t -. !last < 0.1 then true else
+  if not !initialization_complete || t -. !last < 0.2 then true else
   match !cmd with
   | c :: tl ->
     cmd := tl;
@@ -2361,6 +2361,7 @@ let batch s =
       let cmd = Strings.join " " cmd in
       let cmd = Printf.sprintf "import -window \"%s\" -define png:include-chunk=none %s" window_title cmd in
       if Sys.command cmd <> 0 then Printf.eprintf "Batch command failed: %s\n%!" cmd
+    | ["save"] -> send_request Save_req
     | _ -> Printf.eprintf "Unrecognized batch command: %s\n%!" c
     end;
     true