Skip to content

GitLab

why3
why3
Commit 8e4c12d7 authored by Andrei Paskevich's avatar Andrei Paskevich
Browse files
Options

add darkened icons for obsolete goals 

some space tweaks in IDE
parent b0b4f3e6
Hide whitespace changes
Inline Side-by-side
Showing with 76 additions and 41 deletions
src/ide/gconfig.ml
View file @ 8e4c12d7
......@@ -199,6 +199,11 @@ let iconname_unknown = "help32"
let iconname_invalid = "delete32"
let iconname_timeout = "clock32"
let iconname_failure = "bug32"
let iconname_valid_obs = "obsaccept32"
let iconname_unknown_obs = "obshelp32"
let iconname_invalid_obs = "obsdelete32"
let iconname_timeout_obs = "obsclock32"
let iconname_failure_obs = "obsbug32"
let iconname_yes = "accept32"
let iconname_no = "delete32"
let iconname_directory = "folder32"
......@@ -216,6 +221,11 @@ let image_unknown = ref !image_default
let image_invalid = ref !image_default
let image_timeout = ref !image_default
let image_failure = ref !image_default
let image_valid_obs = ref !image_default
let image_unknown_obs = ref !image_default
let image_invalid_obs = ref !image_default
let image_timeout_obs = ref !image_default
let image_failure_obs = ref !image_default
let image_yes = ref !image_default
let image_no = ref !image_default
let image_directory = ref !image_default
......@@ -234,6 +244,11 @@ let resize_images size =
image_invalid := image ~size iconname_invalid;
image_timeout := image ~size iconname_timeout;
image_failure := image ~size iconname_failure;
image_valid_obs := image ~size iconname_valid_obs;
image_unknown_obs := image ~size iconname_unknown_obs;
image_invalid_obs := image ~size iconname_invalid_obs;
image_timeout_obs := image ~size iconname_timeout_obs;
image_failure_obs := image ~size iconname_failure_obs;
image_yes := image ~size iconname_yes;
image_no := image ~size iconname_no;
image_directory := image ~size iconname_directory;
......@@ -249,42 +264,46 @@ let () =
resize_images 20;
eprintf " done.@."
let show_legend_window () =
let dialog = GWindow.dialog ~title:"Why: legend of icons" () in
let vbox = dialog#vbox in
let text = GText.view ~packing:vbox#add () in
let text = GText.view ~packing:vbox#add
~editable:false ~cursor_visible:false () in
let b = text#buffer in
let tt = b#create_tag [`WEIGHT `BOLD; `JUSTIFICATION `CENTER;
`PIXELS_ABOVE_LINES 15; `PIXELS_BELOW_LINES 3; ] in
let i s = b#insert ~iter:b#end_iter s in
let it s = b#insert ~iter:b#end_iter ~tags:[tt] s in
let ib i = b#insert_pixbuf ~iter:b#end_iter ~pixbuf:!i in
i "== icons in the tree view on the left ==\n";
i "\n";
it "Tree view\n";
ib image_directory;
i "A theory, containing a set of goals\n";
i " Theory, containing a set of goals\n";
ib image_file;
i "A goal\n";
i " Goal\n";
ib image_prover;
i "An external prover\n";
i " External prover\n";
ib image_transf;
i "A split transformation\n";
i "\n";
i "== icons in the status column ==\n";
i "\n";
i " Split transformation\n";
it "Status column\n";
ib image_scheduled;
i "external proof scheduled by not started yet\n";
i " Scheduled external proof attempt\n";
ib image_running;
i "external proof is running\n";
i " Running external proof attempt\n";
ib image_valid;
i "goal is proved/theory is fully verified\n";
i " Goal is proved / Theory is fully verified\n";
(*
ib image_invalid;
i " External prover disproved the goal\n";
*)
ib image_timeout;
i "external prover reached the time limit\n";
i " External prover reached the time limit\n";
ib image_unknown;
i "external prover answer was not conclusive\n";
i " External prover answer not conclusive\n";
ib image_failure;
i "external prover call failed\n";
i "\n";
i " External prover call failed\n";
dialog#add_button "Close" `CLOSE ;
let t = b#create_tag [`LEFT_MARGIN 10; `RIGHT_MARGIN 10 ] in
b#apply_tag t ~start:b#start_iter ~stop:b#end_iter;
let ( _ : GWindow.Buttons.about) = dialog#run () in
dialog#destroy ()
......
src/ide/gconfig.mli
View file @ 8e4c12d7
......@@ -75,6 +75,10 @@ val image_valid : GdkPixbuf.pixbuf ref
val image_timeout : GdkPixbuf.pixbuf ref
val image_unknown : GdkPixbuf.pixbuf ref
val image_failure : GdkPixbuf.pixbuf ref
val image_valid_obs : GdkPixbuf.pixbuf ref
val image_timeout_obs : GdkPixbuf.pixbuf ref
val image_unknown_obs : GdkPixbuf.pixbuf ref
val image_failure_obs : GdkPixbuf.pixbuf ref
(*************************)
(* miscellaneous dialogs *)
......
src/ide/gmain.ml
View file @ 8e4c12d7
......@@ -420,11 +420,11 @@ let factory = new GMenu.factory menubar
let accel_group = factory#accel_group
let hb = GPack.hbox ~packing:vbox#add ()
let hb = GPack.hbox ~packing:vbox#add ~border_width:2 ()
let tools_window_vbox =
try
GPack.vbox ~packing:(hb#pack ~expand:false) ()
GPack.vbox ~packing:(hb#pack ~expand:false) ~border_width:2 ()
with Gtk.Error _ -> assert false
let context_frame =
......@@ -432,15 +432,14 @@ let context_frame =
~packing:(tools_window_vbox#pack ~expand:false) ()
let context_box =
GPack.button_box `VERTICAL ~border_width:5
~spacing:5
GPack.button_box `VERTICAL ~border_width:5 ~spacing:5
~packing:context_frame#add ()
let context_unproved_goals_only = ref true
let () =
let b1 = GButton.radio_button
~packing:context_box#add ~label:"Unproved goals only" ()
~packing:context_box#add ~label:"Unproved goals" ()
in
let (_ : GtkSignal.id) =
b1#connect#clicked
......@@ -459,23 +458,26 @@ let provers_frame =
GBin.frame ~label:"Provers"
~packing:(tools_window_vbox#pack ~expand:false) ()
let provers_box = GPack.button_box `VERTICAL ~border_width:5
~spacing:5
let provers_box =
GPack.button_box `VERTICAL ~border_width:5 ~spacing:5
~packing:provers_frame#add ()
let () = provers_frame#set_resize_mode `PARENT
let transf_frame =
GBin.frame ~label:"Transformations"
~packing:(tools_window_vbox#pack ~expand:false) ()
let transf_box =
GPack.button_box `VERTICAL ~border_width:5 ~packing:transf_frame#add ()
GPack.button_box `VERTICAL ~border_width:5 ~spacing:5
~packing:transf_frame#add ()
let tools_frame =
GBin.frame ~label:"Tools"
~packing:(tools_window_vbox#pack ~expand:false) ()
let tools_box = GPack.button_box `VERTICAL ~border_width:5
~spacing:5
let tools_box =
GPack.button_box `VERTICAL ~border_width:5 ~spacing:5
~packing:tools_frame#add ()
let cleaning_frame =
......@@ -483,12 +485,13 @@ let cleaning_frame =
~packing:(tools_window_vbox#pack ~expand:false) ()
let cleaning_box =
GPack.button_box `VERTICAL ~border_width:5 ~packing:cleaning_frame#add ()
GPack.button_box `VERTICAL ~border_width:5 ~spacing:5
~packing:cleaning_frame#add ()
(* horizontal paned *)
let hp = GPack.paned `HORIZONTAL ~border_width:3 ~packing:hb#add ()
let hp = GPack.paned `HORIZONTAL ~packing:hb#add ()
(* tree view *)
......@@ -542,13 +545,18 @@ module Helpers = struct
open Model
let image_of_result = function
| Scheduled -> !image_scheduled
| Running -> !image_running
| Success -> !image_valid
| Timeout -> !image_timeout
| Unknown -> !image_unknown
| HighFailure -> !image_failure
let image_of_result ~obsolete result =
match obsolete,result with
| _, Scheduled -> !image_scheduled
| _, Running -> !image_running
| false, Success -> !image_valid
| false, Timeout -> !image_timeout
| false, Unknown -> !image_unknown
| false, HighFailure -> !image_failure
| true, Success -> !image_valid_obs
| true, Timeout -> !image_timeout_obs
| true, Unknown -> !image_unknown_obs
| true, HighFailure -> !image_failure_obs
let set_file_verified f =
f.file_verified <- true;
......@@ -596,7 +604,8 @@ module Helpers = struct
let set_proof_status ~obsolete a s time =
a.status <- s;
let row = a.proof_row in
goals_model#set ~row ~column:status_column (image_of_result s);
goals_model#set ~row ~column:status_column
(image_of_result ~obsolete s);
let t = if time > 0.0 then
begin
a.Model.time <- time;
......@@ -1499,10 +1508,9 @@ let (_ : GMenu.image_menu_item) =
let vp =
try
GPack.paned `VERTICAL ~border_width:3 ~packing:hp#add ()
GPack.paned `VERTICAL ~packing:hp#add ()
with Gtk.Error _ -> assert false
(******************)
(* goal text view *)
(******************)
......@@ -1511,6 +1519,8 @@ let scrolled_task_view = GBin.scrolled_window
~hpolicy: `AUTOMATIC ~vpolicy: `AUTOMATIC
~packing:vp#add ()
let () = scrolled_task_view#set_shadow_type `ETCHED_OUT
let (_ : GtkSignal.id) =
scrolled_task_view#misc#connect#size_allocate
~callback:
......@@ -1537,6 +1547,8 @@ let scrolled_source_view = GBin.scrolled_window
~packing:vp#add
()
let () = scrolled_source_view#set_shadow_type `ETCHED_OUT
let source_view =
GSourceView2.source_view
~auto_indent:true
......
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