gconfig.ml 40.3 KB
Newer Older
Andrei Paskevich's avatar
Andrei Paskevich committed
1 2 3
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
4
(*  Copyright 2010-2014   --   INRIA - CNRS - Paris-Sud University  *)
Andrei Paskevich's avatar
Andrei Paskevich committed
5 6 7 8 9 10
(*                                                                  *)
(*  This software is distributed under the terms of the GNU Lesser  *)
(*  General Public License version 2.1, with the special exception  *)
(*  on linking described in file LICENSE.                           *)
(*                                                                  *)
(********************************************************************)
MARCHE Claude's avatar
MARCHE Claude committed
11

12
open Why3
13
open Rc
14 15
open Whyconf

16
let debug = Debug.register_info_flag "ide_info"
Andrei Paskevich's avatar
Andrei Paskevich committed
17 18
  ~desc:"Print@ why3ide@ debugging@ messages."

19
let () = Debug.set_flag debug
MARCHE Claude's avatar
MARCHE Claude committed
20

21 22 23 24 25 26 27 28 29 30 31
(** set the exception call back handler to the Exn_printer of why3 *)
let () = (***** TODO TODO make that work, it seems not called!!! *)
  let why3_handler exn =
    Format.eprintf "@[Why3ide callback raised an exception:@\n%a@]@.@."
      Exn_printer.exn_printer exn;
    (** print the stack trace if asked to (can't be done by the usual way) *)
    if Debug.test_flag Debug.stack_trace then
      Printf.eprintf "Backtrace:\n%t\n%!" Printexc.print_backtrace
  in
  GtkSignal.user_handler := why3_handler

32 33
(* config file *)

34
(* type altern_provers = prover option Mprover.t *)
35 36

(** Todo do something generic perhaps*)
37
(*
38 39 40
type conf_replace_prover =
  | CRP_Ask
  | CRP_Not_Obsolete
41
*)
42

43
type t =
MARCHE Claude's avatar
MARCHE Claude committed
44 45 46
    { mutable window_width : int;
      mutable window_height : int;
      mutable tree_width : int;
47
      mutable task_height : int;
MARCHE Claude's avatar
MARCHE Claude committed
48
      mutable verbose : int;
49
      mutable default_prover : string; (* "" means none *)
50
      mutable default_editor : string;
51
      mutable intro_premises : bool;
MARCHE Claude's avatar
MARCHE Claude committed
52
      mutable show_labels : bool;
53
      mutable show_locs : bool;
MARCHE Claude's avatar
MARCHE Claude committed
54
      mutable show_time_limit : bool;
55
      mutable saving_policy : int;
56
      (** 0 = always, 1 = never, 2 = ask *)
Andrei Paskevich's avatar
minor  
Andrei Paskevich committed
57 58
      mutable premise_color : string;
      mutable goal_color : string;
59
      mutable error_color : string;
MARCHE Claude's avatar
MARCHE Claude committed
60
      mutable iconset : string;
61
      (** colors *)
MARCHE Claude's avatar
MARCHE Claude committed
62
      mutable env : Env.env;
63
      mutable config : Whyconf.config;
64
      original_config : Whyconf.config;
65
      (* mutable altern_provers : altern_provers; *)
66
      (* mutable replace_prover : conf_replace_prover; *)
67 68
      (* hidden prover buttons *)
      mutable hidden_provers : string list;
69 70 71
      mutable session_time_limit : int;
      mutable session_mem_limit : int;
      mutable session_nb_processes : int;
MARCHE Claude's avatar
MARCHE Claude committed
72 73
    }

MARCHE Claude's avatar
MARCHE Claude committed
74

75 76 77 78 79 80
type ide = {
  ide_window_width : int;
  ide_window_height : int;
  ide_tree_width : int;
  ide_task_height : int;
  ide_verbose : int;
81 82 83
  ide_intro_premises : bool;
  ide_show_labels : bool;
  ide_show_locs : bool;
MARCHE Claude's avatar
MARCHE Claude committed
84
  ide_show_time_limit : bool;
85
  ide_saving_policy : int;
Andrei Paskevich's avatar
minor  
Andrei Paskevich committed
86 87
  ide_premise_color : string;
  ide_goal_color : string;
88
  ide_error_color : string;
MARCHE Claude's avatar
MARCHE Claude committed
89
  ide_iconset : string;
90
  ide_default_prover : string;
91
  ide_default_editor : string;
92
  (* ide_replace_prover : conf_replace_prover; *)
93
  ide_hidden_provers : string list;
94
}
MARCHE Claude's avatar
MARCHE Claude committed
95

96 97 98 99 100 101
let default_ide =
  { ide_window_width = 1024;
    ide_window_height = 768;
    ide_tree_width = 512;
    ide_task_height = 384;
    ide_verbose = 0;
102 103 104
    ide_intro_premises = true;
    ide_show_labels = false;
    ide_show_locs = false;
MARCHE Claude's avatar
MARCHE Claude committed
105
    ide_show_time_limit = false;
106
    ide_saving_policy = 2;
Andrei Paskevich's avatar
minor  
Andrei Paskevich committed
107 108
    ide_premise_color = "chartreuse";
    ide_goal_color = "gold";
109
    ide_error_color = "orange";
MARCHE Claude's avatar
MARCHE Claude committed
110
    ide_iconset = "boomy";
111
    (* ide_replace_prover = CRP_Ask; *)
112
    ide_default_prover = "";
113
    ide_default_editor =
114 115 116
      (try Sys.getenv "EDITOR" ^ " %f"
       with Not_found -> "editor %f");
    ide_hidden_provers = [];
117 118 119 120 121 122 123 124 125 126 127 128 129
  }

let load_ide section =
  { ide_window_width =
      get_int section ~default:default_ide.ide_window_width "window_width";
    ide_window_height =
      get_int section ~default:default_ide.ide_window_height "window_height";
    ide_tree_width =
      get_int section ~default:default_ide.ide_tree_width "tree_width";
    ide_task_height =
      get_int section ~default:default_ide.ide_task_height "task_height";
    ide_verbose =
      get_int section ~default:default_ide.ide_verbose "verbose";
130
    ide_intro_premises =
François Bobot's avatar
François Bobot committed
131 132
      get_bool section ~default:default_ide.ide_intro_premises
        "intro_premises";
133 134 135 136
    ide_show_labels =
      get_bool section ~default:default_ide.ide_show_labels "print_labels";
    ide_show_locs =
      get_bool section ~default:default_ide.ide_show_locs "print_locs";
MARCHE Claude's avatar
MARCHE Claude committed
137
    ide_show_time_limit =
138 139
      get_bool section ~default:default_ide.ide_show_time_limit
        "print_time_limit";
140 141
    ide_saving_policy =
      get_int section ~default:default_ide.ide_saving_policy "saving_policy";
Andrei Paskevich's avatar
minor  
Andrei Paskevich committed
142 143 144 145 146 147
    ide_premise_color =
      get_string section ~default:default_ide.ide_premise_color
        "premise_color";
    ide_goal_color =
      get_string section ~default:default_ide.ide_goal_color
        "goal_color";
148 149 150
    ide_error_color =
      get_string section ~default:default_ide.ide_error_color
        "error_color";
151
    ide_iconset =
MARCHE Claude's avatar
MARCHE Claude committed
152 153
      get_string section ~default:default_ide.ide_iconset
        "iconset";
154 155 156
    ide_default_editor =
      get_string section ~default:default_ide.ide_default_editor
        "default_editor";
157 158 159
    ide_default_prover =
      get_string section ~default:default_ide.ide_default_prover
        "default_prover";
160 161
 (*
   ide_replace_prover =
162 163
      begin
        match get_stringo section "replace_prover" with
164 165 166
        | None -> default_ide.ide_replace_prover
        | Some "never not obsolete" -> CRP_Not_Obsolete
        | Some "ask" | Some _ -> CRP_Ask
167
      end;
168
 *)
169
    ide_hidden_provers = get_stringl ~default:default_ide.ide_hidden_provers section "hidden_prover";
170
  }
MARCHE Claude's avatar
MARCHE Claude committed
171

172 173 174 175 176 177 178 179 180 181 182

let set_labels_flag =
  let fl = Debug.lookup_flag "print_labels" in
  fun b ->
    (if b then Debug.set_flag else Debug.unset_flag) fl

let set_locs_flag =
  let fl = Debug.lookup_flag "print_locs" in
  fun b ->
    (if b then Debug.set_flag else Debug.unset_flag) fl

183
(* dead code
184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199
let load_altern alterns (_,section) =
  let unknown =
    {prover_name = get_string section "unknown_name";
     prover_version = get_string section "unknown_version";
     prover_altern = get_string ~default:"" section "unknown_alternative"
    } in
  let name = get_stringo section "known_name" in
  let known = match name with
    | None -> None
    | Some name ->
      Some
        {prover_name = name;
         prover_version = get_string section "known_version";
         prover_altern = get_string ~default:"" section "known_alternative";
        } in
  Mprover.add unknown known alterns
200
*)
201

202
let load_config config original_config env =
Andrei Paskevich's avatar
Andrei Paskevich committed
203
  let main = get_main config in
204
  let ide  = match Whyconf.get_section config "ide" with
205
    | None -> default_ide
206 207
    | Some s -> load_ide s
  in
208 209 210
  (* let alterns = *)
  (*   List.fold_left load_altern *)
  (*     Mprover.empty (get_family config "alternative_prover") in *)
211 212
  set_labels_flag ide.ide_show_labels;
  set_locs_flag ide.ide_show_locs;
MARCHE Claude's avatar
MARCHE Claude committed
213 214 215 216 217
  { window_height = ide.ide_window_height;
    window_width  = ide.ide_window_width;
    tree_width    = ide.ide_tree_width;
    task_height   = ide.ide_task_height;
    verbose       = ide.ide_verbose;
218 219 220
    intro_premises= ide.ide_intro_premises ;
    show_labels   = ide.ide_show_labels ;
    show_locs     = ide.ide_show_locs ;
MARCHE Claude's avatar
MARCHE Claude committed
221
    show_time_limit = ide.ide_show_time_limit;
222
    saving_policy = ide.ide_saving_policy ;
Andrei Paskevich's avatar
minor  
Andrei Paskevich committed
223 224
    premise_color = ide.ide_premise_color;
    goal_color = ide.ide_goal_color;
225
    error_color = ide.ide_error_color;
MARCHE Claude's avatar
MARCHE Claude committed
226
    iconset = ide.ide_iconset;
227
    default_prover = ide.ide_default_prover;
MARCHE Claude's avatar
MARCHE Claude committed
228 229
    default_editor = ide.ide_default_editor;
    config         = config;
230
    original_config = original_config;
231
    env            = env;
232
    (* altern_provers = alterns; *)
233
    (* replace_prover = ide.ide_replace_prover; *)
234
    hidden_provers = ide.ide_hidden_provers;
235 236 237 238
    session_time_limit = Whyconf.timelimit main;
    session_mem_limit = Whyconf.memlimit main;
    session_nb_processes = Whyconf.running_provers_max main;
}
MARCHE Claude's avatar
MARCHE Claude committed
239

240

241 242 243
(*

  let save_altern unknown known (id,family) =
244 245 246 247 248 249 250 251 252 253 254 255 256
  let alt = empty_section in
  let alt = set_string alt "unknown_name" unknown.prover_name in
  let alt = set_string alt "unknown_version" unknown.prover_version in
  let alt =
    set_string ~default:"" alt "unknown_alternative" unknown.prover_altern in
  let alt = match known with
    | None -> alt
    | Some known ->
      let alt = set_string alt "known_name" known.prover_name in
      let alt = set_string alt "known_version" known.prover_version in
      set_string ~default:"" alt "known_alternative" known.prover_altern in
  (id+1,(sprintf "alt%i" id,alt)::family)

257 258
  *)

259
(*
260
let debug_save_config n c =
261
  let coq = { prover_name = "Coq" ; prover_version = "8.3pl3";
262 263 264
              prover_altern = "" } in
  let p = Mprover.find coq (get_provers c) in
  let time = Whyconf.timelimit (Whyconf.get_main c) in
265
  Format.eprintf "[debug] save_config %d: timelimit=%d ; editor for Coq=%s@."
266
    n time p.editor
267
*)
268

269
let save_config t =
MARCHE Claude's avatar
MARCHE Claude committed
270
  Debug.dprintf debug "[GUI config] saving IDE config file@.";
271
  (* taking original config, without the extra_config *)
272
  let config = t.original_config in
273 274 275 276 277 278 279 280 281 282
  (* copy possibly modified settings to original config *)
  let new_main = Whyconf.get_main t.config in
  let time = Whyconf.timelimit new_main in
  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
  (* 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
  (* copy also the possibly changed policies *)
283
  let config = set_policies config (get_policies t.config) in
284 285 286 287 288 289
  let ide = empty_section in
  let ide = set_int ide "window_height" t.window_height in
  let ide = set_int ide "window_width" t.window_width in
  let ide = set_int ide "tree_width" t.tree_width in
  let ide = set_int ide "task_height" t.task_height in
  let ide = set_int ide "verbose" t.verbose in
290 291 292
  let ide = set_bool ide "intro_premises" t.intro_premises in
  let ide = set_bool ide "print_labels" t.show_labels in
  let ide = set_bool ide "print_locs" t.show_locs in
MARCHE Claude's avatar
MARCHE Claude committed
293
  let ide = set_bool ide "print_time_limit" t.show_time_limit in
294
  let ide = set_int ide "saving_policy" t.saving_policy in
Andrei Paskevich's avatar
minor  
Andrei Paskevich committed
295 296
  let ide = set_string ide "premise_color" t.premise_color in
  let ide = set_string ide "goal_color" t.goal_color in
297
  let ide = set_string ide "error_color" t.error_color in
MARCHE Claude's avatar
MARCHE Claude committed
298
  let ide = set_string ide "iconset" t.iconset in
299
  let ide = set_string ide "default_prover" t.default_prover in
300
  let ide = set_string ide "default_editor" t.default_editor in
301
  let ide = set_stringl ide "hidden_prover" t.hidden_provers in
302
  let config = Whyconf.set_section config "ide" ide in
303
  Whyconf.save_config config
MARCHE Claude's avatar
MARCHE Claude committed
304

305
let config,load_config =
306 307 308 309 310
  let config = ref None in
  (fun () ->
    match !config with
      | None -> invalid_arg "configuration not yet loaded"
      | Some conf -> conf),
311 312
  (fun conf base_conf env ->
    let c = load_config conf base_conf env in
313
    config := Some c)
314

315
let save_config () = save_config (config ())
316

317
let get_main () = (get_main (config ()).config)
318 319


MARCHE Claude's avatar
MARCHE Claude committed
320 321
(*

MARCHE Claude's avatar
MARCHE Claude committed
322
  images, icons
MARCHE Claude's avatar
MARCHE Claude committed
323 324 325

*)

François Bobot's avatar
François Bobot committed
326 327
let image_default = ref (GdkPixbuf.create ~width:1 ~height:1 ())
(** dumb pixbuf *)
MARCHE Claude's avatar
MARCHE Claude committed
328
let image_undone = ref !image_default
MARCHE Claude's avatar
MARCHE Claude committed
329 330 331 332 333 334
let image_scheduled = ref !image_default
let image_running = ref !image_default
let image_valid = ref !image_default
let image_unknown = ref !image_default
let image_invalid = ref !image_default
let image_timeout = ref !image_default
335
let image_outofmemory = ref !image_default
MARCHE Claude's avatar
MARCHE Claude committed
336
let image_failure = ref !image_default
337 338 339 340
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
341
let image_outofmemory_obs = ref !image_default
342
let image_failure_obs = ref !image_default
MARCHE Claude's avatar
MARCHE Claude committed
343 344 345
let image_yes = ref !image_default
let image_no = ref !image_default
let image_file = ref !image_default
MARCHE Claude's avatar
MARCHE Claude committed
346 347
let image_theory = ref !image_default
let image_goal = ref !image_default
MARCHE Claude's avatar
MARCHE Claude committed
348 349
let image_prover = ref !image_default
let image_transf = ref !image_default
François Bobot's avatar
François Bobot committed
350
let image_metas = ref !image_default
MARCHE Claude's avatar
MARCHE Claude committed
351
let image_editor = ref !image_default
352
let image_replay = ref !image_default
353
let image_cancel = ref !image_default
MARCHE Claude's avatar
MARCHE Claude committed
354
let image_reload = ref !image_default
MARCHE Claude's avatar
merge  
MARCHE Claude committed
355
let image_remove = ref !image_default
356
let image_cleaning = ref !image_default
MARCHE Claude's avatar
MARCHE Claude committed
357

MARCHE Claude's avatar
MARCHE Claude committed
358 359
let why_icon = ref !image_default

MARCHE Claude's avatar
MARCHE Claude committed
360 361
let image ?size f =
  let main = get_main () in
362
  let n =
MARCHE Claude's avatar
MARCHE Claude committed
363 364 365 366 367 368 369 370
    Filename.concat (datadir main)
      (Filename.concat "images" (f^".png"))
  in
  match size with
    | None ->
        GdkPixbuf.from_file n
    | Some s ->
        GdkPixbuf.from_file_at_size ~width:s ~height:s n
371 372 373 374 375 376 377 378 379 380 381 382 383 384 385 386 387 388 389 390

let iconname_default = ref ""
let iconname_undone = ref ""
let iconname_scheduled = ref ""
let iconname_running = ref ""
let iconname_valid = ref ""
let iconname_unknown = ref ""
let iconname_invalid = ref ""
let iconname_timeout = ref ""
let iconname_outofmemory = ref ""
let iconname_failure = ref ""
let iconname_valid_obs = ref ""
let iconname_unknown_obs = ref ""
let iconname_invalid_obs = ref ""
let iconname_timeout_obs = ref ""
let iconname_outofmemory_obs = ref ""
let iconname_failure_obs = ref ""
let iconname_yes = ref ""
let iconname_no = ref ""
let iconname_file = ref ""
MARCHE Claude's avatar
MARCHE Claude committed
391 392
let iconname_theory = ref ""
let iconname_goal = ref ""
393 394
let iconname_prover = ref ""
let iconname_transf = ref ""
François Bobot's avatar
François Bobot committed
395
let iconname_metas  = ref ""
396 397 398 399 400 401 402 403
let iconname_editor = ref ""
let iconname_replay = ref ""
let iconname_cancel = ref ""
let iconname_reload = ref ""
let iconname_remove = ref ""
let iconname_cleaning = ref ""

let load_icon_names () =
MARCHE Claude's avatar
MARCHE Claude committed
404 405
  let ide = config () in
  let iconset = ide.iconset in
406 407 408 409 410 411 412
  let main = get_main () in
  let n =
    Filename.concat (datadir main) (Filename.concat "images" "icons.rc")
  in
  let d = Rc.from_file n in
  let d = Rc.get_family d "iconset" in
  let d = List.assoc iconset d in
MARCHE Claude's avatar
MARCHE Claude committed
413 414 415 416 417 418 419 420 421 422 423 424 425 426 427 428 429 430 431 432 433 434 435 436 437 438
  let get_icon_name n =
    Filename.concat iconset (get_string ~default:"default" d n)
  in
  iconname_default := get_icon_name "default";
  iconname_undone := get_icon_name "undone";
  iconname_scheduled := get_icon_name "scheduled";
  iconname_running := get_icon_name "running";
  iconname_valid := get_icon_name "valid";
  iconname_unknown := get_icon_name "unknown";
  iconname_invalid := get_icon_name "invalid";
  iconname_timeout := get_icon_name "timeout";
  iconname_outofmemory := get_icon_name "outofmemory";
  iconname_failure := get_icon_name "failure";
  iconname_valid_obs := get_icon_name "valid_obs";
  iconname_unknown_obs := get_icon_name "unknown_obs";
  iconname_invalid_obs := get_icon_name "invalid_obs";
  iconname_timeout_obs := get_icon_name "timeout_obs";
  iconname_outofmemory_obs := get_icon_name "outofmemory_obs";
  iconname_failure_obs := get_icon_name "failure_obs";
  iconname_yes := get_icon_name "yes";
  iconname_no := get_icon_name "no";
  iconname_file := get_icon_name "file";
  iconname_theory := get_icon_name "theory";
  iconname_goal := get_icon_name "goal";
  iconname_prover := get_icon_name "prover";
  iconname_transf := get_icon_name "transf";
François Bobot's avatar
François Bobot committed
439
  iconname_metas  := get_icon_name "metas";
MARCHE Claude's avatar
MARCHE Claude committed
440 441 442 443 444 445
  iconname_editor := get_icon_name "editor";
  iconname_replay := get_icon_name "replay";
  iconname_cancel := get_icon_name "cancel";
  iconname_reload := get_icon_name "reload";
  iconname_remove := get_icon_name "remove";
  iconname_cleaning := get_icon_name "cleaning";
446 447
  ()

MARCHE Claude's avatar
MARCHE Claude committed
448
let resize_images size =
449 450 451 452 453 454 455 456 457 458 459 460 461 462 463 464 465 466 467
  image_default := image ~size !iconname_default;
  image_undone := image ~size !iconname_undone;
  image_scheduled := image ~size !iconname_scheduled;
  image_running := image ~size !iconname_running;
  image_valid := image ~size !iconname_valid;
  image_unknown := image ~size !iconname_unknown;
  image_invalid := image ~size !iconname_invalid;
  image_timeout := image ~size !iconname_timeout;
  image_outofmemory := image ~size !iconname_outofmemory;
  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_outofmemory_obs := image ~size !iconname_outofmemory_obs;
  image_failure_obs := image ~size !iconname_failure_obs;
  image_yes := image ~size !iconname_yes;
  image_no := image ~size !iconname_no;
  image_file := image ~size !iconname_file;
MARCHE Claude's avatar
MARCHE Claude committed
468 469
  image_theory := image ~size !iconname_theory;
  image_goal := image ~size !iconname_goal;
470 471
  image_prover := image ~size !iconname_prover;
  image_transf := image ~size !iconname_transf;
François Bobot's avatar
François Bobot committed
472
  image_metas := image ~size !iconname_metas;
473 474 475 476 477 478
  image_editor := image ~size !iconname_editor;
  image_replay := image ~size !iconname_replay;
  image_cancel := image ~size !iconname_cancel;
  image_reload := image ~size !iconname_reload;
  image_remove := image ~size !iconname_remove;
  image_cleaning := image ~size !iconname_cleaning;
MARCHE Claude's avatar
MARCHE Claude committed
479 480
  ()

481
let init () =
MARCHE Claude's avatar
MARCHE Claude committed
482
  Debug.dprintf debug "[GUI config] reading icons...@?";
483
  load_icon_names ();
MARCHE Claude's avatar
MARCHE Claude committed
484
  why_icon := image "logo-why";
MARCHE Claude's avatar
MARCHE Claude committed
485
  resize_images 20;
486
  Debug.dprintf debug " done.@."
MARCHE Claude's avatar
MARCHE Claude committed
487 488

let show_legend_window () =
489 490 491 492 493
  let dialog =
    GWindow.dialog
      ~title:"Why3: legend of icons" ~icon:!why_icon
      ()
  in
MARCHE Claude's avatar
MARCHE Claude committed
494
  let vbox = dialog#vbox in
495 496
  let text = GText.view ~packing:vbox#add
    ~editable:false ~cursor_visible:false () in
MARCHE Claude's avatar
MARCHE Claude committed
497
  let b = text#buffer in
498 499
  let tt = b#create_tag [`WEIGHT `BOLD; `JUSTIFICATION `CENTER;
    `PIXELS_ABOVE_LINES 15; `PIXELS_BELOW_LINES 3; ] in
MARCHE Claude's avatar
MARCHE Claude committed
500
  let i s = b#insert ~iter:b#end_iter s in
501
  let it s = b#insert ~iter:b#end_iter ~tags:[tt] s in
MARCHE Claude's avatar
MARCHE Claude committed
502
  let ib i = b#insert_pixbuf ~iter:b#end_iter ~pixbuf:!i in
503
  it "Tree view\n";
MARCHE Claude's avatar
MARCHE Claude committed
504
  ib image_file;
MARCHE Claude's avatar
MARCHE Claude committed
505 506 507 508
  i "   File, containing a set of theories\n";
  ib image_theory;
  i "   Theory, containing a set of goals\n";
  ib image_goal;
509
  i "   Goal\n";
MARCHE Claude's avatar
MARCHE Claude committed
510
  ib image_prover;
511
  i "   External prover\n";
MARCHE Claude's avatar
MARCHE Claude committed
512
  ib image_transf;
MARCHE Claude's avatar
MARCHE Claude committed
513
  i "   Transformation or strategy\n";
514
  it "Status column\n";
515 516
  ib image_undone;
  i "   External proof attempt not done\n";
MARCHE Claude's avatar
MARCHE Claude committed
517
  ib image_scheduled;
518
  i "   Scheduled external proof attempt\n";
MARCHE Claude's avatar
MARCHE Claude committed
519
  ib image_running;
520
  i "   Running external proof attempt\n";
MARCHE Claude's avatar
MARCHE Claude committed
521
  ib image_valid;
522 523 524
  i "   Goal is proved / Theory is fully verified\n";
  ib image_invalid;
  i "   External prover disproved the goal\n";
MARCHE Claude's avatar
MARCHE Claude committed
525
  ib image_timeout;
526
  i "   External prover reached the time limit\n";
527 528
  ib image_outofmemory;
  i "   External prover ran out of memory\n";
MARCHE Claude's avatar
MARCHE Claude committed
529
  ib image_unknown;
530
  i "   External prover answer not conclusive\n";
MARCHE Claude's avatar
MARCHE Claude committed
531
  ib image_failure;
532
  i "   External prover call failed\n";
533 534 535 536 537 538 539 540
  ib image_valid_obs;
  i "   Valid but obsolete result\n";
  ib image_unknown_obs;
  i "   Answer not conclusive and obsolete\n";
  ib image_invalid_obs;
  i "   Prover disproved goal, but obsolete\n";
  ib image_failure_obs;
  i "   External prover call failed, obsolete\n";
MARCHE Claude's avatar
MARCHE Claude committed
541
  dialog#add_button "Close" `CLOSE ;
542 543
  let t = b#create_tag [`LEFT_MARGIN 10; `RIGHT_MARGIN 10 ] in
  b#apply_tag t ~start:b#start_iter ~stop:b#end_iter;
MARCHE Claude's avatar
MARCHE Claude committed
544 545 546 547 548
  let ( _ : GWindow.Buttons.about) = dialog#run () in
  dialog#destroy ()


let show_about_window () =
MARCHE Claude's avatar
MARCHE Claude committed
549 550
  let about_dialog =
    GWindow.about_dialog
Andrei Paskevich's avatar
Andrei Paskevich committed
551
      ~name:"The Why3 Verification Platform "
MARCHE Claude's avatar
MARCHE Claude committed
552 553 554
      ~authors:["François Bobot";
                "Jean-Christophe Filliâtre";
                "Claude Marché";
Andrei Paskevich's avatar
Andrei Paskevich committed
555 556 557 558 559
                "Guillaume Melquiond";
                "Andrei Paskevich";
                "";
                "with contributions of";
                "";
560
                "Stefan Berghofer";
Andrei Paskevich's avatar
Andrei Paskevich committed
561
                "Sylvie Boldo";
562
                "Martin Clochard";
Andrei Paskevich's avatar
Andrei Paskevich committed
563 564
                "Simon Cruanes";
                "Leon Gondelman";
565
                "Daisuke Ishii";
Andrei Paskevich's avatar
Andrei Paskevich committed
566 567 568 569 570
                "Johannes Kanig";
                "David Mentré";
                "Benjamin Monate";
                "Thi-Minh-Tuyen Nguyen";
                "Simão Melo de Sousa";
571 572 573
                "Asma Tafat";
                "Piotr Trojanek";
                "Makarius Wenzel";
MARCHE Claude's avatar
MARCHE Claude committed
574
               ]
575
      ~copyright:"Copyright 2010-2014 Inria, CNRS, Paris-Sud University"
Andrei Paskevich's avatar
Andrei Paskevich committed
576 577 578
      ~license:"GNU Lesser General Public License version 2.1"
      ~website:"http://why3.lri.fr"
      ~website_label:"http://why3.lri.fr"
MARCHE Claude's avatar
MARCHE Claude committed
579
      ~version:Config.version
MARCHE Claude's avatar
MARCHE Claude committed
580
      ()
MARCHE Claude's avatar
MARCHE Claude committed
581
  in
MARCHE Claude's avatar
MARCHE Claude committed
582 583
  let ( _ : GWindow.Buttons.about) = about_dialog#run () in
  about_dialog#destroy ()
MARCHE Claude's avatar
MARCHE Claude committed
584

585

586

MARCHE Claude's avatar
MARCHE Claude committed
587 588 589

(**** Preferences Window ***)

590
let general_settings (c : t) (notebook:GPack.notebook) =
MARCHE Claude's avatar
MARCHE Claude committed
591 592
  let label = GMisc.label ~text:"General" () in
  let page =
MARCHE Claude's avatar
MARCHE Claude committed
593
    GPack.vbox ~homogeneous:false ~packing:
MARCHE Claude's avatar
MARCHE Claude committed
594
      (fun w -> ignore(notebook#append_page ~tab_label:label#coerce w)) ()
MARCHE Claude's avatar
MARCHE Claude committed
595
  in
596
  (* debug mode ? *)
MARCHE Claude's avatar
MARCHE Claude committed
597
(*
MARCHE Claude's avatar
MARCHE Claude committed
598
  let debugmode =
MARCHE Claude's avatar
MARCHE Claude committed
599
    GButton.check_button ~label:"debug" ~packing:page1#add ()
MARCHE Claude's avatar
MARCHE Claude committed
600 601
      ~active:(c.verbose > 0)
  in
MARCHE Claude's avatar
MARCHE Claude committed
602
  let (_ : GtkSignal.id) =
MARCHE Claude's avatar
MARCHE Claude committed
603 604
    debugmode#connect#toggled ~callback:
      (fun () -> c.verbose <- 1 - c.verbose)
MARCHE Claude's avatar
MARCHE Claude committed
605
  in
MARCHE Claude's avatar
MARCHE Claude committed
606
*)
607 608 609 610 611 612 613
  let external_processes_options_frame =
    GBin.frame ~label:"External provers options"
      ~packing:page#pack ()
  in
  let vb = GPack.vbox ~homogeneous:false
    ~packing:external_processes_options_frame#add ()
  in
614 615
  (* time limit *)
  let width = 200 and xalign = 0.0 in
616 617
  let hb = GPack.hbox ~homogeneous:false ~packing:vb#add ()
  in
618
  let _ = GMisc.label ~text:"Time limit (in sec.): " ~width ~xalign
François Bobot's avatar
François Bobot committed
619
    ~packing:(hb#pack ~expand:false) () in
620
  let timelimit_spin = GEdit.spin_button ~digits:0 ~packing:hb#add () in
621
  timelimit_spin#adjustment#set_bounds ~lower:0. ~upper:42_000_000. ~step_incr:1. ();
622
  timelimit_spin#adjustment#set_value (float_of_int c.session_time_limit);
MARCHE Claude's avatar
MARCHE Claude committed
623
  let (_ : GtkSignal.id) =
624
    timelimit_spin#connect#value_changed ~callback:
625
      (fun () -> c.session_time_limit <- timelimit_spin#value_as_int)
626
  in
627
  (* mem limit *)
628 629
  let hb = GPack.hbox ~homogeneous:false ~packing:vb#add ()
  in
630 631 632 633
  let _ = GMisc.label ~text:"Memory limit (in Mb): " ~width ~xalign
    ~packing:(hb#pack ~expand:false) () in
  let memlimit_spin = GEdit.spin_button ~digits:0 ~packing:hb#add () in
  memlimit_spin#adjustment#set_bounds ~lower:0. ~upper:4000. ~step_incr:100. ();
634
  memlimit_spin#adjustment#set_value (float_of_int c.session_mem_limit);
635 636
  let (_ : GtkSignal.id) =
    memlimit_spin#connect#value_changed ~callback:
637 638 639 640
      (fun () -> c.session_mem_limit <- memlimit_spin#value_as_int)
  in
  (* nb of processes *)
  let hb = GPack.hbox ~homogeneous:false ~packing:vb#add ()
641 642
  in
  let _ = GMisc.label ~text:"Nb of processes: " ~width ~xalign
François Bobot's avatar
François Bobot committed
643
    ~packing:(hb#pack ~expand:false) () in
MARCHE Claude's avatar
MARCHE Claude committed
644
  let nb_processes_spin = GEdit.spin_button ~digits:0 ~packing:hb#add () in
645 646 647
  nb_processes_spin#adjustment#set_bounds
    ~lower:1. ~upper:16. ~step_incr:1. ();
  nb_processes_spin#adjustment#set_value
648
    (float_of_int c.session_nb_processes);
MARCHE Claude's avatar
MARCHE Claude committed
649
  let (_ : GtkSignal.id) =
MARCHE Claude's avatar
MARCHE Claude committed
650
    nb_processes_spin#connect#value_changed ~callback:
651 652 653 654 655 656 657 658 659 660 661 662 663
      (fun () -> c.session_nb_processes <- nb_processes_spin#value_as_int)
  in
  let hb = GPack.hbox ~homogeneous:false ~packing:vb#add () in
  let save_for_future = ref false in
  let save =
    GButton.check_button
      ~label:"save settings above for future sessions"
      ~packing:hb#add ()
      ~active:false
  in
  let (_ : GtkSignal.id) =
    save#connect#toggled ~callback:
      (fun () -> save_for_future := not !save_for_future)
MARCHE Claude's avatar
MARCHE Claude committed
664
  in
665 666
  let display_options_frame =
    GBin.frame ~label:"Display options"
MARCHE Claude's avatar
MARCHE Claude committed
667
      ~packing:page#pack ()
668
  in
669
  (* options for task display *)
670 671 672 673
  let display_options_box =
    GPack.button_box `VERTICAL ~border_width:5 ~spacing:5
      ~packing:display_options_frame#add ()
  in
674 675 676 677 678 679 680 681 682
  let intropremises =
    GButton.check_button ~label:"introduce premises"
      ~packing:display_options_box#add ()
      ~active:c.intro_premises
  in
  let (_ : GtkSignal.id) =
    intropremises#connect#toggled ~callback:
      (fun () -> c.intro_premises <- not c.intro_premises)
  in
683
  let showlabels =
684 685
    GButton.check_button
      ~label:"show labels in formulas"
686
      ~packing:display_options_box#add ()
687
      ~active:c.show_labels
688 689 690
  in
  let (_ : GtkSignal.id) =
    showlabels#connect#toggled ~callback:
691 692
      (fun () ->
         c.show_labels <- not c.show_labels;
693 694
         set_labels_flag c.show_labels)
  in
695
  let showlocs =
696 697
    GButton.check_button
      ~label:"show source locations in formulas"
698
      ~packing:display_options_box#add ()
699
      ~active:c.show_locs
700 701 702
  in
  let (_ : GtkSignal.id) =
    showlocs#connect#toggled ~callback:
703 704
      (fun () ->
         c.show_locs <- not c.show_locs;
705 706
         set_locs_flag c.show_locs)
  in
MARCHE Claude's avatar
MARCHE Claude committed
707 708
  let showtimelimit =
    GButton.check_button
Claude Marche's avatar
Claude Marche committed
709
      ~label:"show time and memory limits for each proof"
MARCHE Claude's avatar
MARCHE Claude committed
710 711 712 713 714 715 716 717
      ~packing:display_options_box#add ()
      ~active:c.show_time_limit
  in
  let (_ : GtkSignal.id) =
    showtimelimit#connect#toggled ~callback:
      (fun () ->
         c.show_time_limit <- not c.show_time_limit)
  in
718
  (* session saving policy *)
719
  let set_saving_policy n () = c.saving_policy <- n in
720 721
  let saving_policy_frame =
    GBin.frame ~label:"Session saving policy"
MARCHE Claude's avatar
MARCHE Claude committed
722
      ~packing:page#pack ()
723 724
  in
  let saving_policy_box =
725 726
    GPack.button_box
      `VERTICAL ~border_width:5 ~spacing:5
727 728
      ~packing:saving_policy_frame#add ()
  in
729 730
  let choice0 =
    GButton.radio_button
731
      ~label:"always save on exit"
732
      ~active:(c.saving_policy = 0)
733
      ~packing:saving_policy_box#pack ()
734 735 736
  in
  let choice1 =
    GButton.radio_button
737
      ~label:"never save on exit" ~group:choice0#group
738
      ~active:(c.saving_policy = 1)
739
      ~packing:saving_policy_box#pack ()
740 741 742
  in
  let choice2 =
    GButton.radio_button
743 744
      ~label:"ask whether to save on exit" ~group:choice0#group
      ~active:(c.saving_policy = 2)
745
      ~packing:saving_policy_box#pack ()
746
  in
747 748 749 750 751 752 753 754 755
  let (_ : GtkSignal.id) =
    choice0#connect#toggled ~callback:(set_saving_policy 0)
  in
  let (_ : GtkSignal.id) =
    choice1#connect#toggled ~callback:(set_saving_policy 1)
  in
  let (_ : GtkSignal.id) =
    choice2#connect#toggled ~callback:(set_saving_policy 2)
  in
756
  let (_ : GPack.box) =
MARCHE Claude's avatar
MARCHE Claude committed
757 758
    GPack.vbox ~packing:(page#pack ~expand:true) ()
  in
759
  save_for_future
MARCHE Claude's avatar
MARCHE Claude committed
760 761 762 763 764 765 766 767 768

(* Page "Provers" *)

let provers_page c (notebook:GPack.notebook) =
  let label = GMisc.label ~text:"Provers" () in
  let page =
    GPack.vbox ~homogeneous:false ~packing:
      (fun w -> ignore(notebook#append_page ~tab_label:label#coerce w)) ()
  in
MARCHE Claude's avatar
MARCHE Claude committed
769 770 771 772 773 774 775 776
  let hbox = GPack.hbox ~packing:(page#pack ~fill:true ~expand:true) () in
  let scrollview =
  try
    GBin.scrolled_window ~hpolicy:`NEVER ~vpolicy:`AUTOMATIC
      ~packing:(hbox#pack ~fill:true ~expand:true) ()
  with Gtk.Error _ -> assert false
  in let () = scrollview#set_shadow_type `OUT in
  let vbox = GPack.vbox ~packing:scrollview#add_with_viewport () in
777 778
  let hbox = GPack.hbox ~packing:(vbox#pack ~fill:true ~expand:true) () in
  (* show/hide provers *)
MARCHE Claude's avatar
MARCHE Claude committed
779
  let frame =
780 781
    GBin.frame ~label:"Prover button in the left toolbar"
      ~packing:(hbox#pack ~fill:true ~expand:true) () in
MARCHE Claude's avatar
MARCHE Claude committed
782 783
  let provers_box =
    GPack.button_box `VERTICAL ~border_width:5 ~spacing:5
784
      ~packing:frame#add () in
MARCHE Claude's avatar
MARCHE Claude committed
785 786 787
  let hidden_provers = Hashtbl.create 7 in
  Mprover.iter
    (fun _ p ->
788 789 790 791
      let name = prover_parseable_format p.prover in
      let label = Pp.string_of_wnl print_prover p.prover in
      let hidden = ref (List.mem name c.hidden_provers) in
      Hashtbl.add hidden_provers name hidden;
MARCHE Claude's avatar
MARCHE Claude committed
792 793 794 795 796 797 798 799 800 801 802
      let b =
        GButton.check_button ~label ~packing:provers_box#add ()
          ~active:(not !hidden)
      in
      let (_ : GtkSignal.id) =
        b#connect#toggled ~callback:
          (fun () -> hidden := not !hidden;
            c.hidden_provers <-
              Hashtbl.fold
              (fun l h acc -> if !h then l::acc else acc) hidden_provers [])
      in ())
803 804 805 806 807 808 809 810 811 812 813 814 815 816 817 818 819 820 821 822 823
    (Whyconf.get_provers c.config);
  (* default prover *)
  let frame2 =
    GBin.frame ~label:"Default prover"
      ~packing:(hbox#pack ~fill:true ~expand:true) () in
  let provers_box =
    GPack.button_box `VERTICAL ~border_width:5 ~spacing:5
      ~packing:frame2#add () in
  let group = ref None in
  Mprover.iter
    (fun _ p ->
      let name = prover_parseable_format p.prover in
      let label = Pp.string_of_wnl print_prover p.prover in
      let b =
        GButton.radio_button ~label ?group:!group ~packing:provers_box#add ()
          ~active:(name = c.default_prover)
      in
      if !group = None then group := Some b#group;
      let (_ : GtkSignal.id) =
        b#connect#toggled ~callback:(fun () -> c.default_prover <- name)
      in ())
MARCHE Claude's avatar
MARCHE Claude committed
824
    (Whyconf.get_provers c.config)
MARCHE Claude's avatar
MARCHE Claude committed
825

826 827


MARCHE Claude's avatar
MARCHE Claude committed
828 829 830 831 832 833 834 835 836 837 838 839 840 841 842 843 844 845 846 847 848 849 850 851 852 853 854 855 856 857 858 859 860 861 862 863 864 865 866 867 868 869 870 871 872 873
(* Page "Uninstalled provers" *)

let alternatives_frame c (notebook:GPack.notebook) =
  let label = GMisc.label ~text:"Uninstalled provers" () in
  let page =
    GPack.vbox ~homogeneous:false ~packing:
      (fun w -> ignore(notebook#append_page ~tab_label:label#coerce w)) ()
  in
  let frame =
    GBin.frame ~label:"Click to remove a setting"
      ~packing:page#pack ()
  in
  let box =
    GPack.button_box `VERTICAL ~border_width:5 ~spacing:5
      ~packing:frame#add ()
  in
  let remove button p () =
    button#destroy ();
    c.config <- set_policies c.config (Mprover.remove p (get_policies c.config))
  in
  let iter p policy =
    let label =
      match policy with
        | CPU_keep -> Pp.sprintf_wnl "proofs with %a kept as they are" print_prover p
        | CPU_upgrade t ->
          Pp.sprintf_wnl "proofs with %a moved to %a" print_prover p print_prover t
        | CPU_duplicate t ->
          Pp.sprintf_wnl "proofs with %a duplicated to %a" print_prover p print_prover t
    in
    let button = GButton.button ~label ~packing:box#add () in
    let (_ : GtkSignal.id) =
      button#connect#released ~callback:(remove button p)
    in ()
  in
  Mprover.iter iter (get_policies c.config);
  let _fillbox =
    GPack.vbox ~packing:(page#pack ~expand:true) ()
  in
  ()

let editors_page c (notebook:GPack.notebook) =
  let label = GMisc.label ~text:"Editors" () in
  let page =
    GPack.vbox ~homogeneous:false ~packing:
      (fun w -> ignore(notebook#append_page ~tab_label:label#coerce w)) ()
  in
MARCHE Claude's avatar
MARCHE Claude committed
874 875 876 877 878 879
  let hbox = GPack.hbox ~packing:(page#pack ~expand:true ~fill:true) () in
  let scrollview =
    GBin.scrolled_window ~hpolicy:`NEVER ~vpolicy:`AUTOMATIC
      ~packing:(hbox#pack ~fill:true ~expand:true) ()
  in
  let vbox = GPack.vbox ~packing:scrollview#add_with_viewport () in
MARCHE Claude's avatar
MARCHE Claude committed
880
  let default_editor_frame =
MARCHE Claude's avatar
MARCHE Claude committed
881
    GBin.frame ~label:"Default editor" ~packing:vbox#pack ()
MARCHE Claude's avatar
MARCHE Claude committed
882 883 884 885 886 887 888 889
  in
  let editor_entry =
   GEdit.entry ~text:c.default_editor ~packing:default_editor_frame#add ()
  in
  let (_ : GtkSignal.id) =
    editor_entry#connect#changed ~callback:
      (fun () -> c.default_editor <- editor_entry#text)
  in
MARCHE Claude's avatar
MARCHE Claude committed
890 891 892 893
  let frame =
    GBin.frame ~label:"Specific editors"
      ~packing:vbox#pack ()
  in
MARCHE Claude's avatar
MARCHE Claude committed
894
  let box = GPack.vbox ~border_width:5 ~packing:frame#add () in
895
  let editors = Whyconf.get_editors c.config in
MARCHE Claude's avatar
MARCHE Claude committed
896
  let _,strings,indexes,map =
897
    Meditor.fold
898
      (fun k data (i,str,ind,map) ->
MARCHE Claude's avatar
MARCHE Claude committed
899 900 901
        let n = data.editor_name in
        (i+1, n::str, Meditor.add k i ind, Meditor.add n k map))
      editors (2, [], Meditor.empty, Meditor.empty)
902
  in
MARCHE Claude's avatar
MARCHE Claude committed
903
  let strings = "(default)" :: "--" :: (List.rev strings) in
904
  let add_prover p pi =
905
    let text = Pp.string_of_wnl Whyconf.print_prover p in
906
    let hb = GPack.hbox ~homogeneous:false ~packing:box#pack () in
907 908
    let _ = GMisc.label ~width:150 ~xalign:0.0 ~text
      ~packing:(hb#pack ~fill:true ~expand:true) () in
909 910 911 912 913 914 915 916 917 918 919 920 921 922
    let (combo, ((_ : GTree.list_store), column)) =
      GEdit.combo_box_text ~packing:hb#pack ~strings ()
    in
    combo#set_row_separator_func
      (Some (fun m row -> m#get ~row ~column = "--"));
    let i =
      try Meditor.find pi.editor indexes with Not_found -> 0
    in
    combo#set_active i;
    let ( _ : GtkSignal.id) = combo#connect#changed
      ~callback:(fun () ->
        match combo#active_iter with
          | None -> ()
          | Some row ->
923
	    let data =
924
              match combo#model#get ~row ~column with
MARCHE Claude's avatar
MARCHE Claude committed
925
                | "(default)" -> ""
926 927
                | s ->
                  try Meditor.find s map
MARCHE Claude's avatar
MARCHE Claude committed
928
                  with Not_found -> assert false
929
            in
930
	    (* Debug.dprintf debug "prover %a : selected editor '%s'@." *)
931
            (*   print_prover p data; *)
932 933 934 935 936 937 938
            let provers = Whyconf.get_provers c.config in
            c.config <-
              Whyconf.set_provers c.config
              (Mprover.add p { pi with editor = data} provers)
      )
    in
    ()
MARCHE Claude's avatar
MARCHE Claude committed
939
  in
MARCHE Claude's avatar
MARCHE Claude committed
940
  Mprover.iter add_prover (Whyconf.get_provers c.config)
MARCHE Claude's avatar
MARCHE Claude committed
941 942


943
let preferences (c : t) =
944
  let dialog = GWindow.dialog
MARCHE Claude's avatar
MARCHE Claude committed
945
    ~modal:true ~icon:(!why_icon)
946 947
    ~title:"Why3: preferences" ()
  in
MARCHE Claude's avatar
MARCHE Claude committed
948 949 950
  let vbox = dialog#vbox in
  let notebook = GPack.notebook ~packing:vbox#add () in
  (** page "general settings" **)
951
  let save_for_future_session = general_settings c notebook in
MARCHE Claude's avatar
MARCHE Claude committed
952 953 954 955 956
  (*** page "editors" **)
  editors_page c notebook;
  (** page "Provers" **)
  provers_page c notebook;
  (*** page "uninstalled provers" *)
957
  alternatives_frame c notebook;
MARCHE Claude's avatar
MARCHE Claude committed
958 959 960 961 962 963 964 965 966 967 968 969 970 971 972
  (** page "Colors" **)
(*
  let label2 = GMisc.label ~text:"Colors" () in
  let _color_sel = GMisc.color_selection (* ~title:"Goal color" *)
    ~show:true
    ~packing:(fun w -> ignore(notebook#append_page
                                ~tab_label:label2#coerce w)) ()
  in
  let (_ : GtkSignal.id) =
    color_sel#connect ColorSelection.S.color_changed ~callback:
      (fun c -> Format.eprintf "Gconfig.color_sel : %s@."
         c)
  in
*)
  (** bottom button **)
MARCHE Claude's avatar
MARCHE Claude committed
973 974
  dialog#add_button "Close" `CLOSE ;
  let ( _ : GWindow.Buttons.about) = dialog#run () in
975 976 977 978 979
  (* let config = set_main config *)
  (*   (set_limits (get_main config) *)
  (*      t.time_limit t.mem_limit t.max_running_processes) *)
  (* in *)

980 981 982 983
  if !save_for_future_session then
    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);
984
  save_config ();
MARCHE Claude's avatar
MARCHE Claude committed
985
  dialog#destroy ()
986

987
(*
988
let run_auto_detection gconfig =
989 990
  let config = Autodetection.run_auto_detection gconfig.config in
  gconfig.config <- config;
991 992
  let _provers = get_provers config in
(* TODO: store the result differently
993 994
  gconfig.provers <- Mstr.fold (Session.get_prover_data gconfig.env) provers
  Mstr.empty
995 996
*)
  ()
997
*)
MARCHE Claude's avatar
MARCHE Claude committed
998

MARCHE Claude's avatar
MARCHE Claude committed
999
(*let () = Debug.dprintf debug "[GUI config] end of configuration initialization@."*)
1000

1001 1002
let uninstalled_prover c eS unknown =
  try
1003
    Whyconf.get_prover_upgrade_policy c.config unknown
1004
  with Not_found ->
1005 1006
    let others,names,versions = Session_tools.unknown_to_known_provers
      (Whyconf.get_provers eS.Session.whyconf) unknown in
1007
    let dialog = GWindow.dialog
1008
      ~icon:(!why_icon) ~modal:true
1009 1010
      ~title:"Why3: Uninstalled prover" ()
    in
1011
    let vbox = dialog#vbox in
1012
    let hb = GPack.hbox ~packing:vbox#add () in
MARCHE Claude's avatar
MARCHE Claude committed
1013
    let _ = GMisc.image ~stock:`DIALOG_WARNING ~packing:hb#add () in
1014 1015 1016 1017
    let text =
      Pp.sprintf "The prover %a is not installed"
        Whyconf.print_prover unknown
    in
MARCHE Claude's avatar
MARCHE Claude committed
1018
    let _ = GMisc.label ~ypad:20 ~text ~xalign:0.5 ~packing:hb#add () in
1019
    let label = "Please select a policy for associated proof attempts" in
1020 1021 1022 1023 1024 1025 1026 1027 1028 1029
    let policy_frame = GBin.frame ~label ~packing:vbox#add () in
    let choice = ref 0 in
    let prover_choosed = ref None in
    let set_prover prover () = prover_choosed := Some prover in
    let box =
      GPack.button_box `VERTICAL ~border_width:5 ~spacing:5
        ~packing:policy_frame#add ()
    in
    let choice0 = GButton.radio_button
      ~label:"keep proofs as they are, do not try to play them"
1030
      ~active:true
1031 1032 1033 1034 1035 1036 1037 1038 1039 1040
      ~packing:box#add () in
    let choice1 = GButton.radio_button
      ~label:"move proofs to the selected prover below"
      ~active:false ~group:choice0#group
      ~packing:box#add () in
    let choice2 = GButton.radio_button
      ~label:"duplicate proofs to the selected prover below"
      ~active:false ~group:choice0#group
      ~packing:box#add () in
    let first = ref None in
1041
    let alternatives_section acc label alternatives =
1042 1043 1044 1045
      if alternatives <> [] then
        let frame = GBin.frame ~label ~packing:vbox#add () in
        let box =
          GPack.button_box `VERTICAL ~border_width:5 ~spacing:5
MARCHE Claude's avatar
MARCHE Claude committed
1046
            ~packing:(vbox#pack ~fill:true ~expand:true) ()
1047 1048 1049 1050 1051 1052 1053 1054 1055 1056 1057 1058 1059 1060 1061 1062 1063 1064 1065 1066 1067
        in
        let iter_alter prover =
          let choice =
            let label = Pp.string_of_wnl print_prover prover in
            match !first with
              | None ->
                let choice =
                  GButton.radio_button ~label ~active:true ~packing:box#add ()
                in
                prover_choosed := Some prover;
                first := Some choice;
                choice
              | Some first ->
                GButton.radio_button ~label ~group:first#group
                  ~active:false ~packing:box#add ()
          in
          ignore (choice#connect#toggled ~callback:(set_prover prover))
        in
        List.iter iter_alter alternatives;
        frame#misc :: (* box#misc :: *) acc
      else acc
1068
    in
1069 1070 1071 1072 1073 1074 1075 1076 1077 1078 1079 1080
    let boxes = alternatives_section [] "Same name and same version" versions in
    let boxes = alternatives_section boxes "Same name and different version" names in
    let boxes = alternatives_section boxes "Different name" others in
    let hide_provers () = List.iter (fun b -> b#set_sensitive false) boxes in
    let show_provers () = List.iter (fun b -> b#set_sensitive true) boxes in
    hide_provers ();
    ignore (choice0#connect#toggled
              ~callback:(fun () -> choice := 0; hide_provers ()));
    ignore (choice1#connect#toggled
              ~callback:(fun () -> choice := 1; show_provers ()));
    ignore (choice2#connect#toggled
              ~callback:(fun () -> choice := 2; show_provers ()));
1081 1082 1083 1084 1085 1086 1087 1088 1089 1090 1091 1092 1093 1094
    dialog#add_button "Ok" `CLOSE ;
    ignore (dialog#run ());
    dialog#destroy ();
    let policy =
      match !choice, !prover_choosed with
        | 0,_ -> CPU_keep
        | 1, Some p -> CPU_upgrade p
        | 2, Some p -> CPU_duplicate p
        | _ -> assert false
    in
    c.config <- set_prover_upgrade_policy c.config unknown policy;
    policy
(*
let unknown_prover c eS unknown =
1095 1096 1097 1098 1099