Mise à jour terminée. Pour connaître les apports de la version 13.8.4 par rapport à notre ancienne version vous pouvez lire les "Release Notes" suivantes :
https://about.gitlab.com/releases/2021/02/11/security-release-gitlab-13-8-4-released/
https://about.gitlab.com/releases/2021/02/05/gitlab-13-8-3-released/

Commit a526c45d authored by MARCHE Claude's avatar MARCHE Claude

IDE: context menu now contains more or less the items that were in the left...

IDE: context menu now contains more or less the items that were in the left toolbar in former versions of Why3
parent 19a6fb9e
......@@ -315,18 +315,27 @@ transformations have changed (new version of \why), \why will detect
that. Since the provers might answer differently on these new
proof obligations, the corresponding proof attempts are marked obsolete.
\subsection{Context Menu}
\subsection{Menus}
The left toolbar that was present in former versions of Why3 is now
replaced by a context menu activited by clicking the right mouse button,
while cursor is on a given row of the proof session tree.
\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[Edit] starts an editor on the selected task.
\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.
\item[Remove] removes a proof attempt or a transformation.
\item[Clean] removes any unsuccessful proof attempt for which there is
another successful proof attempt for the same goal
\item[Interrupt] cancels all the proof attempts currently scheduled or running.
\end{description}
\subsection{Global Menus}
\begin{description}
\item[Menu \textsf{File}]\emptyitem
\begin{description}
\item[Add File to session] adds a file in the current proof session.
......@@ -392,8 +401,7 @@ proof obligations, the corresponding proof attempts are marked obsolete.
\item[Mark obsolete] marks all the proof as
obsolete. This allows to replay every proof.
\item[Interrupt] cancels all the proof attempts currently scheduled
but not yet started.
\item[Interrupt] cancels all the proof attempts currently scheduled or running.
\item[Bisect] performs a reduction of the context for the the current selected proof attempt, which must be a Valid one.
......@@ -445,6 +453,29 @@ available as a textual command. However the textual interface allows
for much more possibilities, including the ability to invoke
transformations with arguments.
\subsection{Key shortcuts}
\begin{itemize}
\item Save session and files : ctrl+s
\item Save all and refresh session: ctrl+r
\item Quit : ctrl+q
\item Enlarge font : ctrl+plus
\item Reduce font : ctrl+minus
\item Collapse proven goals : !
\item Collapse current node : -
\item Expand current node : +
\item Copy : ctrl+c
\item Paste : ctrl+v
\item Select parent node : ctrl+up
\item Select next unproven goal : ctrl+down
\item Change focus to command line : return
\item Edit : e
\item Replay : r
\item Clean : c
\item Remove : del
\item Mark obsolete : o
\end{itemize}
\subsection{Preferences Dialog}
......
......@@ -2201,6 +2201,13 @@ let complete_context_menu () =
~callback:(on_selected_rows ~multiple:false ~notif_kind:"Unfocus_req error" ~action:"unfocus"
(fun id -> Command_req (id, "Unfocus")));
let ( _ : GMenu.menu_item) = context_tools_factory#add_separator () in
let context_edit_menu_item =
create_menu_item context_tools_factory "Edit"
"View or edit proof script (shortcut: e)" in
connect_menu_item
context_edit_menu_item
~callback:(on_selected_rows ~multiple:false ~notif_kind:"Edit error" ~action:"edit"
(fun id -> Command_req (id, "edit")));
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
......@@ -2215,6 +2222,27 @@ let complete_context_menu () =
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")));
let context_remove_item =
create_menu_item context_tools_factory "Remove"
"Remove the selected proof attempts or transformations (shortcut: del)" in
connect_menu_item
context_remove_item
~callback:(on_selected_rows ~multiple:true ~notif_kind:"Remove_subtree error" ~action:"remove"
(fun id -> Remove_subtree id));
let context_clean_menu_item =
create_menu_item context_tools_factory "Clean"
"Remove unsuccessful proofs or transformations that are below a proved goal (shortcut: c)" in
connect_menu_item
context_clean_menu_item
~callback:(on_selected_rows ~multiple:false ~notif_kind:"Clean error" ~action:"clean"
(fun id -> Command_req (id, "clean")));
let context_interrupt_item =
create_menu_item context_tools_factory "Interrupt"
"Stop all running proof attempts" in
connect_menu_item
context_interrupt_item
~callback:(on_selected_rows ~multiple:true ~notif_kind:"Interrupt error" ~action:"interrupt"
(fun id -> Command_req (id, "interrupt")));
()
......
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