Commit 84905664 authored by MARCHE Claude's avatar MARCHE Claude

adding replay commands in the context menu

fixed doc
parent 4582aecd
......@@ -319,6 +319,13 @@ proof obligations, the corresponding proof attempts are marked obsolete.
\subsection{Menus}
\begin{description}
\item[Context menu]\emptyitem This menu is selected by the mouse right button on some row of the task tree view.
\begin{description}
\item[provers] The detected provers are listed. Note that you can hide some provers of that list using the preferences, tab \textsf{Provers}.
\item[strategies] the set of known strategies is listed
\item[Replay valid obsolete proofs] all proof nodes below the selected nodes that are obsolete but whose former status was Valid are replayed.
\item[Replay all obsolete proofs] all proof nodes below the selected nodes that are obsolete are replayed.
\end{description}
\item[Menu \textsf{File}]\emptyitem
\begin{description}
\item[Add File] adds a file in the GUI.
......
......@@ -81,8 +81,7 @@ You are now ready to call provers on the goals
-{}-detect-provers}}.
%END LATEX
%HEVEA {} (If not done yet, you must perform prover autodetection using \texttt{why3 config -{}-detect-provers}.)
A prover is selected using the context menu (right-click), in the
\texttt{Provers} sub-menu.
A prover is selected using the context menu (right-click).
This prover is then called on the goal selected
in the tree view. You can select several goals at a time, either
by using multi-selection (typically by clicking while pressing the
......@@ -111,13 +110,12 @@ obvious here it will not succeed.
Instead of calling a prover on a goal, you can apply a transformation
to it. Since $G_2$ is a conjunction, a possibility is to split it
into subgoals. You can do that by selecting \textsf{Split VC} in the
\texttt{Strategies} sub-menu of the context menu. Now you have two
subgoals, and you can try again a prover on them, for example
Alt-Ergo. 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}.
context menu. Now you have two subgoals, and you can try again a
prover on them, for example Alt-Ergo. 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 3;type next;type split_vc;wait 1;snap -crop 1024x384+0+0 doc/gui-4.png;save;wait 1" doc/hello_proof.why
\begin{figure}[tbp]
......@@ -129,7 +127,7 @@ displayed on Figure~\ref{fig:gui4}.
The first part of goal $G_2$ is still unproved. As a last resort, we
can try to call the Coq proof assistant, by selecting it in the
\texttt{Provers} list.
context menu.
A new sub-row appear for Coq, and the Coq proof editor is launched.
(It is \texttt{coqide} by default; see
Section~\ref{sec:ideref} for details on how to configure this). You get
......@@ -217,7 +215,7 @@ reminds us that $G_2$ is not proved.
You may want to clean some the proof attempts, \eg removing the
unsuccessful ones when a project is finally fully proved.
A proof or a transformation can be removed by selecting it and
using menu \textsf{Tools/Remove} or key \texttt{Suppr}.
using menu \textsf{Tools/Remove} or the \texttt{Delete} key.
It performs an automatic removal of all proofs
attempts that are unsuccessful, while there exists a successful proof
attempt for the same goal.
......
......@@ -950,7 +950,7 @@ let provers_page c (notebook:GPack.notebook) =
let hbox_pack = hbox#pack ~fill:true ~expand:true ?from:None ?padding:None in
(* show/hide provers *)
let frame =
GBin.frame ~label:"Provers visible in the contextual menu" ~packing:hbox_pack ()
GBin.frame ~label:"Provers visible in the context menu" ~packing:hbox_pack ()
in
let provers_box =
GPack.button_box `VERTICAL ~border_width:5 ~spacing:5
......
......@@ -2073,8 +2073,13 @@ let () =
edit_menu_item#add_accelerator ~group:tools_accel_group ~modi:[] GdkKeysyms._e
let replay_menu_item =
create_menu_item tools_factory "Replay obsolete"
"Replay all obsolete proofs (shortcut: r)"
create_menu_item tools_factory "Replay valid obsolete proofs"
"Replay valid obsolete proofs below the current node (shortcut: r)"
let replay_all_menu_item =
create_menu_item tools_factory "Replay all obsolete proofs"
"Replay all obsolete proofs below the current node"
let () =
replay_menu_item#add_accelerator ~group:tools_accel_group ~modi:[] GdkKeysyms._r
......@@ -2121,7 +2126,7 @@ let paste_item = create_menu_item tools_factory "Paste"
"Paste the copied node below the current node"
let () =
let complete_context_menu () =
let on_selected_rows ~multiple ~notif_kind ~action f () =
match get_selected_row_references () with
| [] ->
......@@ -2137,6 +2142,10 @@ let () =
replay_menu_item
~callback:(on_selected_rows ~multiple:false ~notif_kind:"Replay error" ~action:"replay"
(fun id -> Command_req (id, "replay")));
connect_menu_item
replay_all_menu_item
~callback:(on_selected_rows ~multiple:false ~notif_kind:"Replay error" ~action:"replay all"
(fun id -> Command_req (id, "replay all")));
connect_menu_item
clean_menu_item
~callback:(on_selected_rows ~multiple:false ~notif_kind:"Clean error" ~action:"clean"
......@@ -2164,7 +2173,24 @@ let () =
connect_menu_item
unfocus_item
~callback:(on_selected_rows ~multiple:false ~notif_kind:"Unfocus_req error" ~action:"unfocus"
(fun id -> Command_req (id, "Unfocus")))
(fun id -> Command_req (id, "Unfocus")));
let ( _ : GMenu.menu_item) = context_tools_factory#add_separator () in
let replay_context_menu_item =
create_menu_item context_tools_factory "Replay valid obsolete proofs"
"Replay valid obsolete proofs below the current node (shortcut: r)" in
connect_menu_item
replay_context_menu_item
~callback:(on_selected_rows ~multiple:false ~notif_kind:"Replay error" ~action:"replay"
(fun id -> Command_req (id, "replay")));
let replay_all_context_menu_item =
create_menu_item context_tools_factory "Replay all obsolete proofs"
"Replay all obsolete proofs below the current node" in
connect_menu_item
replay_all_context_menu_item
~callback:(on_selected_rows ~multiple:false ~notif_kind:"Replay error" ~action:"replay all"
(fun id -> Command_req (id, "replay all")));
()
(*************************************)
......@@ -2317,6 +2343,7 @@ let treat_notification n =
main_window#show ();
display_warnings ();
init_completion g_info.provers g_info.transformations g_info.strategies g_info.commands;
complete_context_menu ();
Opt.iter goals_view#selection#select_iter goals_model#get_iter_first
| Saved ->
session_needs_saving := false;
......
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