Attention une mise à jour du service Gitlab va être effectuée le mardi 30 novembre entre 17h30 et 18h00. Cette mise à jour va générer une interruption du service dont nous ne maîtrisons pas complètement la durée mais qui ne devrait pas excéder quelques minutes. Cette mise à jour intermédiaire en version 14.0.12 nous permettra de rapidement pouvoir mettre à votre disposition une version plus récente.

Commit 9651a7b9 authored by MARCHE Claude's avatar MARCHE Claude
Browse files

goal removal in IDE

parent b880ebf6
...@@ -40,7 +40,9 @@ ...@@ -40,7 +40,9 @@
** semantics not clear, should be clarified, documented and ** semantics not clear, should be clarified, documented and
implemented accordingly implemented accordingly
* add transf "inline goal" (TODO, not urgent) * add transf "inline goal" (TODO, not urgent)
* add button "remove" (TODO: implement) * add button "remove"
** removing goals: done, but status need update
** removing transformation: (TODO: implement)
* add button "replay" (TODO, not urgent) * add button "replay" (TODO, not urgent)
** semantics: replay obsolete proofs ** semantics: replay obsolete proofs
......
...@@ -218,7 +218,8 @@ the actions of the various menus and buttons of the interface. ...@@ -218,7 +218,8 @@ the actions of the various menus and buttons of the interface.
\item[Replay] replay all obsolete proofs [NOT YET AVAILABLE] \item[Replay] replay all obsolete proofs [NOT YET AVAILABLE]
\item[Remove] Remove a proof attempt or a transformation. [NOT YET AVAILABLE] \item[Remove] Remove a proof attempt or a transformation.
[Removing transformation NOT YET AVAILABLE]
\end{description} \end{description}
......
...@@ -502,7 +502,7 @@ let task_checksum t = ...@@ -502,7 +502,7 @@ let task_checksum t =
Digest.to_hex (Digest.string s) Digest.to_hex (Digest.string s)
let info_window mt s = let info_window ?(callback=(fun () -> ())) mt s =
let buttons = match mt with let buttons = match mt with
| `INFO -> GWindow.Buttons.close | `INFO -> GWindow.Buttons.close
| `WARNING -> GWindow.Buttons.close | `WARNING -> GWindow.Buttons.close
...@@ -516,12 +516,11 @@ let info_window mt s = ...@@ -516,12 +516,11 @@ let info_window mt s =
~title:"Why3 info or error" ~title:"Why3 info or error"
~show:true () ~show:true ()
in in
let r = ref false in
let (_ : GtkSignal.id) = let (_ : GtkSignal.id) =
d#connect#response d#connect#response
~callback:(function x -> r := x = `OK; d#destroy ()) ~callback:(function x -> d#destroy ();
in if x = `OK then callback ())
!r in ()
module Helpers = struct module Helpers = struct
...@@ -1211,7 +1210,7 @@ let select_file () = ...@@ -1211,7 +1210,7 @@ let select_file () =
"@[Error while reading file@ '%s':@ %a@]" f "@[Error while reading file@ '%s':@ %a@]" f
Exn_printer.exn_printer e; Exn_printer.exn_printer e;
let msg = flush_str_formatter () in let msg = flush_str_formatter () in
let (_:bool) = info_window `ERROR msg in () info_window `ERROR msg
end end
| `DELETE_EVENT | `CANCEL -> () | `DELETE_EVENT | `CANCEL -> ()
end ; end ;
...@@ -1219,7 +1218,7 @@ let select_file () = ...@@ -1219,7 +1218,7 @@ let select_file () =
let not_implemented () = let not_implemented () =
let (_:bool) = info_window `INFO "This feature is not yet implemented, sorry" in () info_window `INFO "This feature is not yet implemented, sorry"
(*************) (*************)
(* File menu *) (* File menu *)
...@@ -1442,7 +1441,7 @@ let () = ...@@ -1442,7 +1441,7 @@ let () =
in () in ()
let () = let () =
let b = GButton.button ~packing:transf_box#add ~label:"Inline" () in let b = GButton.button ~packing:transf_box#add ~label:"(Inline)" () in
(* (*
let i = GMisc.image ~pixbuf:(!image_transf) () in let i = GMisc.image ~pixbuf:(!image_transf) () in
let () = b#set_image i#coerce in let () = b#set_image i#coerce in
...@@ -1720,9 +1719,7 @@ let edit_current_proof () = ...@@ -1720,9 +1719,7 @@ let edit_current_proof () =
| [] -> () | [] -> ()
| [r] -> edit_selected_row r | [r] -> edit_selected_row r
| _ -> | _ ->
let (_:bool) = info_window `INFO "Please select exactly one proof to edit"
info_window `INFO "Please select exactly one proof to edit"
in ()
let add_item_edit () = let add_item_edit () =
...@@ -1745,7 +1742,7 @@ let () = ...@@ -1745,7 +1742,7 @@ let () =
in () in ()
let () = let () =
let b = GButton.button ~packing:tools_box#add ~label:"Replay" () in let b = GButton.button ~packing:tools_box#add ~label:"(Replay)" () in
(* (*
let i = GMisc.image ~pixbuf:(!image_replay) () in let i = GMisc.image ~pixbuf:(!image_replay) () in
let () = b#set_image i#coerce in let () = b#set_image i#coerce in
...@@ -1766,28 +1763,25 @@ let confirm_remove_row r = ...@@ -1766,28 +1763,25 @@ let confirm_remove_row r =
let row = filter_model#get_iter r in let row = filter_model#get_iter r in
match filter_model#get ~row ~column:Model.index_column with match filter_model#get ~row ~column:Model.index_column with
| Model.Row_goal _g -> | Model.Row_goal _g ->
let (_:bool) = info_window `ERROR "Cannot remove a goal" in () info_window `ERROR "Cannot remove a goal"
| Model.Row_theory _th -> | Model.Row_theory _th ->
let (_:bool) = info_window `ERROR "Cannot remove a theory" in () info_window `ERROR "Cannot remove a theory"
| Model.Row_file _file -> | Model.Row_file _file ->
let (_:bool) = info_window `ERROR "Cannot remove a file" in () info_window `ERROR "Cannot remove a file"
| Model.Row_proof_attempt a -> | Model.Row_proof_attempt a ->
let b = info_window
info_window `QUESTION ~callback:(fun () -> remove_proof_attempt a)
"Do you really want to remove the selected proof attempt?" `QUESTION
in "Do you really want to remove the selected proof attempt?"
if b then remove_proof_attempt a
| Model.Row_transformation _tr -> | Model.Row_transformation _tr ->
let (_:bool) = info_window `INFO "Transformation removal not implemented" in () info_window `INFO "Transformation removal not yet available, sorry"
let confirm_remove_selection () = let confirm_remove_selection () =
match goals_view#selection#get_selected_rows with match goals_view#selection#get_selected_rows with
| [] -> () | [] -> ()
| [r] -> confirm_remove_row r | [r] -> confirm_remove_row r
| _ -> | _ ->
let (_:bool) = info_window `INFO "Please select exactly one item to remove"
info_window `INFO "Please select exactly one item to remove"
in ()
let () = let () =
let b = GButton.button ~packing:cleaning_box#add ~label:"Remove" () in let b = GButton.button ~packing:cleaning_box#add ~label:"Remove" () in
......
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