Setting whether counter-example should be get in why3ide is done by in GUI -...

Setting whether counter-example should be get in why3ide is done by in GUI - instead of setting this using command-line option.

src/driver/whyconf.ml

@@ -175,6 +175,8 @@ type main = {
   (* max number of running prover processes *)
   plugins : string list;
   (* plugins to load, without extension, relative to [libdir]/plugins *)
+  cntexample : bool;
+  (* true provers should be asked for counter-example model *)
 }
 
 let libdir m =
@@ -203,6 +205,7 @@ let loadpath m =
 let timelimit m = m.timelimit
 let memlimit m = m.memlimit
 let running_provers_max m = m.running_provers_max
+let cntexample m = m.cntexample
 
 exception StepsCommandNotSpecified of string
 
@@ -219,6 +222,9 @@ let get_complete_command pc steplimit =
 let set_limits m time mem running =
   { m with timelimit = time; memlimit = mem; running_provers_max = running }
 
+let set_cntexample m cntexample =
+  { m with cntexample = cntexample }
+
 let plugins m = m.plugins
 let set_plugins m pl =
   (* TODO : sanitize? *)
@@ -258,6 +264,7 @@ let empty_main =
     memlimit = 1000; (* 1 Mb *)
     running_provers_max = 2; (* two provers run in parallel *)
     plugins = [];
+    cntexample = true;
   }
 
 let default_main =
@@ -276,6 +283,7 @@ let set_main rc main =
   let section =
     set_int section "running_provers_max" main.running_provers_max in
   let section = set_stringl section "plugin" main.plugins in
+  let section = set_bool section "cntexample" main.cntexample in
   set_section rc "main" section
 
 exception NonUniqueId
@@ -509,6 +517,7 @@ let load_main dirname section =
     running_provers_max = get_int ~default:default_main.running_provers_max
       section "running_provers_max";
     plugins = get_stringl ~default:[] section "plugin";
+    cntexample = get_bool ~default:default_main.cntexample section "cntexample"
   }
 
 let read_config_rc conf_file =

src/driver/whyconf.mli

@@ -75,7 +75,9 @@ val loadpath: main -> string list
 val timelimit: main -> int
 val memlimit: main -> int
 val running_provers_max: main -> int
+val cntexample: main -> bool
 val set_limits: main -> int -> int -> int -> main
+val set_cntexample: main -> bool -> main
 
 val plugins : main -> string list
 val pluginsdir : main -> string

src/ide/gconfig.ml

@@ -61,6 +61,7 @@ type t =
       mutable session_time_limit : int;
       mutable session_mem_limit : int;
       mutable session_nb_processes : int;
+      mutable session_cntexample : bool;
     }
 
 
@@ -210,6 +211,7 @@ let load_config config original_config env =
     session_time_limit = Whyconf.timelimit main;
     session_mem_limit = Whyconf.memlimit main;
     session_nb_processes = Whyconf.running_provers_max main;
+    session_cntexample = Whyconf.cntexample main;
 }
 
 let save_config t =
@@ -222,6 +224,9 @@ let save_config t =
   let mem = Whyconf.memlimit new_main in
   let nb = Whyconf.running_provers_max new_main in
   let config = set_main config (set_limits (get_main config) time mem nb) in
+  let new_main = Whyconf.get_main t.config in
+  let cntexample = Whyconf.cntexample new_main in
+  let config = set_main config (set_cntexample (get_main config) cntexample) in
   (* copy also provers section since it may have changed (the editor
      can be set via the preferences dialog) *)
   let config = set_provers config (get_provers t.config) in
@@ -628,6 +633,15 @@ let general_settings (c : t) (notebook:GPack.notebook) =
     nb_processes_spin#connect#value_changed ~callback:
       (fun () -> c.session_nb_processes <- nb_processes_spin#value_as_int)
   in
+  (* counter-example *)
+  let cntexample_check = GButton.check_button ~label:"get counter-example"
+    ~packing:vb#add ()
+    ~active:c.session_cntexample
+  in
+  let (_: GtkSignal.id) =
+    cntexample_check#connect#toggled ~callback:
+      (fun () -> c.session_cntexample <- not c.session_cntexample)
+  in
   (* session saving policy *)
   let set_saving_policy n () = c.saving_policy <- n in
   let saving_policy_frame =
@@ -1046,6 +1060,9 @@ let preferences (c : t) =
       c.config <- Whyconf.set_main c.config
         (Whyconf.set_limits (Whyconf.get_main c.config)
            c.session_time_limit c.session_mem_limit c.session_nb_processes);
+      c.config <- Whyconf.set_main c.config
+	(Whyconf.set_cntexample (Whyconf.get_main c.config)
+	   c.session_cntexample);
       save_config ()
     | `CLOSE | `DELETE_EVENT -> ()
   end;

src/ide/gconfig.mli

@@ -40,6 +40,7 @@ type t =
       mutable session_time_limit : int;
       mutable session_mem_limit : int;
       mutable session_nb_processes : int;
+      mutable session_cntexample : bool;
     }
 
 val load_config : Whyconf.config -> Whyconf.config -> Why3.Env.env -> unit

src/ide/gmain.ml

@@ -39,15 +39,12 @@ let debug = Debug.lookup_flag "ide_info"
 
 let files = Queue.create ()
 let opt_parser = ref None
-let opt_cntexmp = ref false
 
 let spec = Arg.align [
   "-F", Arg.String (fun s -> opt_parser := Some s),
       "<format> select input format (default: \"why\")";
   "--format", Arg.String (fun s -> opt_parser := Some s),
       " same as -F";
-  "--get-ce", Arg.Set opt_cntexmp,
-      " gets the counter-example model";
 (*
   "-f",
    Arg.String (fun s -> input_files := s :: !input_files),
@@ -994,6 +991,7 @@ let () = Queue.iter (open_file ~start:true) files
 let prover_on_selected_goals pr =
   let timelimit = gconfig.session_time_limit in
   let memlimit = gconfig.session_mem_limit in
+  let cntexample = Whyconf.cntexample (Whyconf.get_main gconfig.config) in
   List.iter
     (fun row ->
       try
@@ -1001,7 +999,7 @@ let prover_on_selected_goals pr =
        M.run_prover
          (env_session()) sched
          ~context_unproved_goals_only:!context_unproved_goals_only
-         ~cntexample:!opt_cntexmp ~timelimit ~memlimit
+         ~cntexample ~timelimit ~memlimit
          pr a
       with e ->
         eprintf "@[Exception raised while running a prover:@ %a@.@]"
@@ -1076,6 +1074,7 @@ let bisect_proof_attempt pa =
   let timelimit = ref (-1) in
   let set_timelimit res =
     timelimit := 1 + (int_of_float (floor res.Call_provers.pr_time)) in
+  let cntexample = Whyconf.cntexample (Whyconf.get_main gconfig.config) in
   let rec callback lp pa c = function
     | S.Running | S.Scheduled -> ()
     | S.Interrupted ->
@@ -1107,14 +1106,14 @@ let bisect_proof_attempt pa =
         let npa = S.copy_external_proof ~notify ~keygen ~obsolete:true
           ~goal ~env_session:eS pa in
         MA.init_any (S.Metas metas);
-        M.run_external_proof eS sched ~cntexample:!opt_cntexmp npa
+        M.run_external_proof eS sched ~cntexample npa
         with e ->
           dprintf debug "Bisecting error:@\n%a@."
             Exn_printer.exn_printer e end
       | Eliminate_definition.BSstep (t,c) ->
         assert (not lp.S.prover_config.C.in_place); (* TODO do this case *)
         M.schedule_proof_attempt
-	  ~cntexample:!opt_cntexmp
+	  ~cntexample
           ~timelimit:!timelimit
           ~memlimit:pa.S.proof_memlimit
 	  ~steplimit:(-1)
@@ -1153,7 +1152,7 @@ let bisect_proof_attempt pa =
             dprintf debug "Prover can't be loaded.@."
           | Some lp ->
             M.schedule_proof_attempt
-	      ~cntexample:!opt_cntexmp
+	      ~cntexample
               ~timelimit:!timelimit
               ~memlimit:pa.S.proof_memlimit
 	      ~steplimit:(-1)
@@ -1164,7 +1163,7 @@ let bisect_proof_attempt pa =
               ~callback:(callback lp pa c) sched t in
   dprintf debug "Bisecting with %a started.@."
     C.print_prover pa.S.proof_prover;
-  M.run_external_proof eS sched ~cntexample:!opt_cntexmp ~callback:first_callback pa
+  M.run_external_proof eS sched ~cntexample ~callback:first_callback pa
 
 let apply_bisect_on_selection () =
   List.iter
@@ -2131,6 +2130,7 @@ let edit_selected_row r =
         ()
     | S.Proof_attempt a ->
         let e = env_session () in
+	let cntexample = Whyconf.cntexample (Whyconf.get_main gconfig.config) in
 (*
         let coq = { prover_name = "Coq" ; prover_version = "8.3pl3";
                     prover_altern = "" } in
@@ -2141,7 +2141,7 @@ let edit_selected_row r =
           "[debug] save_config %d: timelimit=%d ; editor for Coq=%s@."
           0 time p.editor;
 *)
-        M.edit_proof ~cntexample:!opt_cntexmp e sched ~default_editor:gconfig.default_editor a
+        M.edit_proof ~cntexample e sched ~default_editor:gconfig.default_editor a
     | S.Transf _ -> ()
     | S.Metas _ -> ()