gconfig.ml 41.2 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;
MARCHE Claude's avatar
MARCHE Claude committed
55
      mutable max_boxes : int;
56
      mutable saving_policy : int;
57
      (** 0 = always, 1 = never, 2 = ask *)
Andrei Paskevich's avatar
minor  
Andrei Paskevich committed
58 59
      mutable premise_color : string;
      mutable goal_color : string;
60
      mutable error_color : string;
MARCHE Claude's avatar
MARCHE Claude committed
61
      mutable iconset : string;
62
      (** colors *)
MARCHE Claude's avatar
MARCHE Claude committed
63
      mutable env : Env.env;
64
      mutable config : Whyconf.config;
65
      original_config : Whyconf.config;
66
      (* mutable altern_provers : altern_provers; *)
67
      (* mutable replace_prover : conf_replace_prover; *)
68 69
      (* hidden prover buttons *)
      mutable hidden_provers : string list;
70 71 72
      mutable session_time_limit : int;
      mutable session_mem_limit : int;
      mutable session_nb_processes : int;
MARCHE Claude's avatar
MARCHE Claude committed
73 74
    }

MARCHE Claude's avatar
MARCHE Claude committed
75

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

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

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";
133
    ide_intro_premises =
François Bobot's avatar
François Bobot committed
134 135
      get_bool section ~default:default_ide.ide_intro_premises
        "intro_premises";
136 137 138 139
    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
140
    ide_show_time_limit =
141 142
      get_bool section ~default:default_ide.ide_show_time_limit
        "print_time_limit";
MARCHE Claude's avatar
MARCHE Claude committed
143 144 145
    ide_max_boxes =
      get_int section ~default:default_ide.ide_max_boxes
        "max_boxes";
146 147
    ide_saving_policy =
      get_int section ~default:default_ide.ide_saving_policy "saving_policy";
Andrei Paskevich's avatar
minor  
Andrei Paskevich committed
148 149 150 151 152 153
    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";
154 155 156
    ide_error_color =
      get_string section ~default:default_ide.ide_error_color
        "error_color";
157
    ide_iconset =
MARCHE Claude's avatar
MARCHE Claude committed
158 159
      get_string section ~default:default_ide.ide_iconset
        "iconset";
160 161 162
    ide_default_editor =
      get_string section ~default:default_ide.ide_default_editor
        "default_editor";
163 164 165
    ide_default_prover =
      get_string section ~default:default_ide.ide_default_prover
        "default_prover";
166 167
 (*
   ide_replace_prover =
168 169
      begin
        match get_stringo section "replace_prover" with
170 171 172
        | None -> default_ide.ide_replace_prover
        | Some "never not obsolete" -> CRP_Not_Obsolete
        | Some "ask" | Some _ -> CRP_Ask
173
      end;
174
 *)
175
    ide_hidden_provers = get_stringl ~default:default_ide.ide_hidden_provers section "hidden_prover";
176
  }
MARCHE Claude's avatar
MARCHE Claude committed
177

178 179 180 181 182 183 184 185 186 187 188

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

189
(* dead code
190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205
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
206
*)
207

208
let load_config config original_config env =
Andrei Paskevich's avatar
Andrei Paskevich committed
209
  let main = get_main config in
210
  let ide  = match Whyconf.get_section config "ide" with
211
    | None -> default_ide
212 213
    | Some s -> load_ide s
  in
214 215 216
  (* let alterns = *)
  (*   List.fold_left load_altern *)
  (*     Mprover.empty (get_family config "alternative_prover") in *)
217 218
  set_labels_flag ide.ide_show_labels;
  set_locs_flag ide.ide_show_locs;
MARCHE Claude's avatar
MARCHE Claude committed
219 220 221 222 223
  { 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;
224 225 226
    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
227
    show_time_limit = ide.ide_show_time_limit;
MARCHE Claude's avatar
MARCHE Claude committed
228
    max_boxes = ide.ide_max_boxes;
229
    saving_policy = ide.ide_saving_policy ;
Andrei Paskevich's avatar
minor  
Andrei Paskevich committed
230 231
    premise_color = ide.ide_premise_color;
    goal_color = ide.ide_goal_color;
232
    error_color = ide.ide_error_color;
MARCHE Claude's avatar
MARCHE Claude committed
233
    iconset = ide.ide_iconset;
234
    default_prover = ide.ide_default_prover;
MARCHE Claude's avatar
MARCHE Claude committed
235 236
    default_editor = ide.ide_default_editor;
    config         = config;
237
    original_config = original_config;
238
    env            = env;
239
    (* altern_provers = alterns; *)
240
    (* replace_prover = ide.ide_replace_prover; *)
241
    hidden_provers = ide.ide_hidden_provers;
242 243 244 245
    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
246

247

248 249 250
(*

  let save_altern unknown known (id,family) =
251 252 253 254 255 256 257 258 259 260 261 262 263
  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)

264 265
  *)

266
(*
267
let debug_save_config n c =
268
  let coq = { prover_name = "Coq" ; prover_version = "8.3pl3";
269 270 271
              prover_altern = "" } in
  let p = Mprover.find coq (get_provers c) in
  let time = Whyconf.timelimit (Whyconf.get_main c) in
272
  Format.eprintf "[debug] save_config %d: timelimit=%d ; editor for Coq=%s@."
273
    n time p.editor
274
*)
275

276
let save_config t =
MARCHE Claude's avatar
MARCHE Claude committed
277
  Debug.dprintf debug "[GUI config] saving IDE config file@.";
278
  (* taking original config, without the extra_config *)
279
  let config = t.original_config in
280 281 282 283 284 285 286 287 288 289
  (* 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 *)
290
  let config = set_policies config (get_policies t.config) in
291 292 293 294 295 296
  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
297 298 299
  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
300
  let ide = set_bool ide "print_time_limit" t.show_time_limit in
MARCHE Claude's avatar
MARCHE Claude committed
301
  let ide = set_int ide "max_boxes" t.max_boxes in
302
  let ide = set_int ide "saving_policy" t.saving_policy in
Andrei Paskevich's avatar
minor  
Andrei Paskevich committed
303 304
  let ide = set_string ide "premise_color" t.premise_color in
  let ide = set_string ide "goal_color" t.goal_color in
305
  let ide = set_string ide "error_color" t.error_color in
MARCHE Claude's avatar
MARCHE Claude committed
306
  let ide = set_string ide "iconset" t.iconset in
307
  let ide = set_string ide "default_prover" t.default_prover in
308
  let ide = set_string ide "default_editor" t.default_editor in
309
  let ide = set_stringl ide "hidden_prover" t.hidden_provers in
310
  let config = Whyconf.set_section config "ide" ide in
311
  Whyconf.save_config config
MARCHE Claude's avatar
MARCHE Claude committed
312

313
let config,load_config =
314 315 316 317 318
  let config = ref None in
  (fun () ->
    match !config with
      | None -> invalid_arg "configuration not yet loaded"
      | Some conf -> conf),
319 320
  (fun conf base_conf env ->
    let c = load_config conf base_conf env in
321
    config := Some c)
322

323
let save_config () = save_config (config ())
324

325
let get_main () = (get_main (config ()).config)
326 327


MARCHE Claude's avatar
MARCHE Claude committed
328 329
(*

MARCHE Claude's avatar
MARCHE Claude committed
330
  images, icons
MARCHE Claude's avatar
MARCHE Claude committed
331 332 333

*)

François Bobot's avatar
François Bobot committed
334 335
let image_default = ref (GdkPixbuf.create ~width:1 ~height:1 ())
(** dumb pixbuf *)
MARCHE Claude's avatar
MARCHE Claude committed
336
let image_undone = ref !image_default
MARCHE Claude's avatar
MARCHE Claude committed
337 338 339 340 341 342
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
343
let image_outofmemory = ref !image_default
MARCHE Claude's avatar
MARCHE Claude committed
344
let image_failure = ref !image_default
345 346 347 348
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
349
let image_outofmemory_obs = ref !image_default
350
let image_failure_obs = ref !image_default
MARCHE Claude's avatar
MARCHE Claude committed
351 352 353
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
354 355
let image_theory = ref !image_default
let image_goal = ref !image_default
MARCHE Claude's avatar
MARCHE Claude committed
356 357
let image_prover = ref !image_default
let image_transf = ref !image_default
François Bobot's avatar
François Bobot committed
358
let image_metas = ref !image_default
MARCHE Claude's avatar
MARCHE Claude committed
359
let image_editor = ref !image_default
360
let image_replay = ref !image_default
361
let image_cancel = ref !image_default
MARCHE Claude's avatar
MARCHE Claude committed
362
let image_reload = ref !image_default
MARCHE Claude's avatar
merge  
MARCHE Claude committed
363
let image_remove = ref !image_default
364
let image_cleaning = ref !image_default
MARCHE Claude's avatar
MARCHE Claude committed
365

MARCHE Claude's avatar
MARCHE Claude committed
366 367
let why_icon = ref !image_default

MARCHE Claude's avatar
MARCHE Claude committed
368 369
let image ?size f =
  let main = get_main () in
370
  let n =
MARCHE Claude's avatar
MARCHE Claude committed
371 372 373 374 375 376 377 378
    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
379 380 381 382 383 384 385 386 387 388 389 390 391 392 393 394 395 396 397 398

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
399 400
let iconname_theory = ref ""
let iconname_goal = ref ""
401 402
let iconname_prover = ref ""
let iconname_transf = ref ""
François Bobot's avatar
François Bobot committed
403
let iconname_metas  = ref ""
404 405 406 407 408 409 410 411
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
412 413
  let ide = config () in
  let iconset = ide.iconset in
414 415 416 417 418 419 420
  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
421 422 423 424 425 426 427 428 429 430 431 432 433 434 435 436 437 438 439 440 441 442 443 444 445 446
  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
447
  iconname_metas  := get_icon_name "metas";
MARCHE Claude's avatar
MARCHE Claude committed
448 449 450 451 452 453
  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";
454 455
  ()

MARCHE Claude's avatar
MARCHE Claude committed
456
let resize_images size =
457 458 459 460 461 462 463 464 465 466 467 468 469 470 471 472 473 474 475
  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
476 477
  image_theory := image ~size !iconname_theory;
  image_goal := image ~size !iconname_goal;
478 479
  image_prover := image ~size !iconname_prover;
  image_transf := image ~size !iconname_transf;
François Bobot's avatar
François Bobot committed
480
  image_metas := image ~size !iconname_metas;
481 482 483 484 485 486
  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
487 488
  ()

489
let init () =
MARCHE Claude's avatar
MARCHE Claude committed
490
  Debug.dprintf debug "[GUI config] reading icons...@?";
491
  load_icon_names ();
MARCHE Claude's avatar
MARCHE Claude committed
492
  why_icon := image "logo-why";
MARCHE Claude's avatar
MARCHE Claude committed
493
  resize_images 20;
494
  Debug.dprintf debug " done.@."
MARCHE Claude's avatar
MARCHE Claude committed
495 496

let show_legend_window () =
497 498 499 500 501
  let dialog =
    GWindow.dialog
      ~title:"Why3: legend of icons" ~icon:!why_icon
      ()
  in
MARCHE Claude's avatar
MARCHE Claude committed
502
  let vbox = dialog#vbox in
503 504
  let text = GText.view ~packing:vbox#add
    ~editable:false ~cursor_visible:false () in
MARCHE Claude's avatar
MARCHE Claude committed
505
  let b = text#buffer in
506 507
  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
508
  let i s = b#insert ~iter:b#end_iter s in
509
  let it s = b#insert ~iter:b#end_iter ~tags:[tt] s in
MARCHE Claude's avatar
MARCHE Claude committed
510
  let ib i = b#insert_pixbuf ~iter:b#end_iter ~pixbuf:!i in
511
  it "Tree view\n";
MARCHE Claude's avatar
MARCHE Claude committed
512
  ib image_file;
MARCHE Claude's avatar
MARCHE Claude committed
513 514 515 516
  i "   File, containing a set of theories\n";
  ib image_theory;
  i "   Theory, containing a set of goals\n";
  ib image_goal;
517
  i "   Goal\n";
MARCHE Claude's avatar
MARCHE Claude committed
518
  ib image_prover;
519
  i "   External prover\n";
MARCHE Claude's avatar
MARCHE Claude committed
520
  ib image_transf;
MARCHE Claude's avatar
MARCHE Claude committed
521
  i "   Transformation or strategy\n";
522
  it "Status column\n";
523 524
  ib image_undone;
  i "   External proof attempt not done\n";
MARCHE Claude's avatar
MARCHE Claude committed
525
  ib image_scheduled;
526
  i "   Scheduled external proof attempt\n";
MARCHE Claude's avatar
MARCHE Claude committed
527
  ib image_running;
528
  i "   Running external proof attempt\n";
MARCHE Claude's avatar
MARCHE Claude committed
529
  ib image_valid;
530 531 532
  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
533
  ib image_timeout;
534
  i "   External prover reached the time limit\n";
535 536
  ib image_outofmemory;
  i "   External prover ran out of memory\n";
MARCHE Claude's avatar
MARCHE Claude committed
537
  ib image_unknown;
538
  i "   External prover answer not conclusive\n";
MARCHE Claude's avatar
MARCHE Claude committed
539
  ib image_failure;
540
  i "   External prover call failed\n";
541 542 543 544 545 546 547 548
  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
549
  dialog#add_button "Close" `CLOSE ;
550 551
  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
552 553 554 555 556
  let ( _ : GWindow.Buttons.about) = dialog#run () in
  dialog#destroy ()


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

593

594

MARCHE Claude's avatar
MARCHE Claude committed
595 596 597

(**** Preferences Window ***)

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

(* 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
790 791 792 793 794 795 796 797
  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
798 799
  let hbox = GPack.hbox ~packing:(vbox#pack ~fill:true ~expand:true) () in
  (* show/hide provers *)
MARCHE Claude's avatar
MARCHE Claude committed
800
  let frame =
801 802
    GBin.frame ~label:"Prover button in the left toolbar"
      ~packing:(hbox#pack ~fill:true ~expand:true) () in
MARCHE Claude's avatar
MARCHE Claude committed
803 804
  let provers_box =
    GPack.button_box `VERTICAL ~border_width:5 ~spacing:5
805
      ~packing:frame#add () in
MARCHE Claude's avatar
MARCHE Claude committed
806 807 808
  let hidden_provers = Hashtbl.create 7 in
  Mprover.iter
    (fun _ p ->
809 810 811 812
      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
813 814 815 816 817 818 819 820 821 822 823
      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 ())
824 825 826 827 828 829 830 831 832 833 834 835 836 837 838 839 840 841 842 843 844
    (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
845
    (Whyconf.get_provers c.config)
MARCHE Claude's avatar
MARCHE Claude committed
846

847 848


MARCHE Claude's avatar
MARCHE Claude committed
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 874 875 876 877 878 879 880 881 882 883 884 885 886 887 888 889 890 891 892 893 894
(* 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
895 896 897 898 899 900
  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
901
  let default_editor_frame =
MARCHE Claude's avatar
MARCHE Claude committed
902
    GBin.frame ~label:"Default editor" ~packing:vbox#pack ()
MARCHE Claude's avatar
MARCHE Claude committed
903 904 905 906 907 908 909 910
  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
911 912 913 914
  let frame =
    GBin.frame ~label:"Specific editors"
      ~packing:vbox#pack ()
  in
MARCHE Claude's avatar
MARCHE Claude committed
915
  let box = GPack.vbox ~border_width:5 ~packing:frame#add () in
916
  let editors = Whyconf.get_editors c.config in
MARCHE Claude's avatar
MARCHE Claude committed
917
  let _,strings,indexes,map =
918
    Meditor.fold
919
      (fun k data (i,str,ind,map) ->
MARCHE Claude's avatar
MARCHE Claude committed
920 921 922
        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)
923
  in
MARCHE Claude's avatar
MARCHE Claude committed
924
  let strings = "(default)" :: "--" :: (List.rev strings) in
925
  let add_prover p pi =
926
    let text = Pp.string_of_wnl Whyconf.print_prover p in
927
    let hb = GPack.hbox ~homogeneous:false ~packing:box#pack () in
928 929
    let _ = GMisc.label ~width:150 ~xalign:0.0 ~text
      ~packing:(hb#pack ~fill:true ~expand:true) () in
930 931 932 933 934 935 936 937 938 939 940 941 942 943
    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 ->
944
	    let data =
945
              match combo#model#get ~row ~column with
MARCHE Claude's avatar
MARCHE Claude committed
946
                | "(default)" -> ""
947 948
                | s ->
                  try Meditor.find s map
MARCHE Claude's avatar
MARCHE Claude committed
949
                  with Not_found -> assert false
950
            in
951
	    (* Debug.dprintf debug "prover %a : selected editor '%s'@." *)
952
            (*   print_prover p data; *)
953 954 955 956 957 958 959
            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
960
  in
MARCHE Claude's avatar
MARCHE Claude committed
961
  Mprover.iter add_prover (Whyconf.get_provers c.config)
MARCHE Claude's avatar
MARCHE Claude committed
962 963


964
let preferences (c : t) =
965
  let dialog = GWindow.dialog
MARCHE Claude's avatar
MARCHE Claude committed
966
    ~modal:true ~icon:(!why_icon)
967 968
    ~title:"Why3: preferences" ()
  in
MARCHE Claude's avatar
MARCHE Claude committed
969 970 971
  let vbox = dialog#vbox in
  let notebook = GPack.notebook ~packing:vbox#add () in
  (** page "general settings" **)
972
  let save_for_future_session = general_settings c notebook in
MARCHE Claude's avatar
MARCHE Claude committed
973 974 975 976 977
  (*** page "editors" **)
  editors_page c notebook;
  (** page "Provers" **)
  provers_page c notebook;
  (*** page "uninstalled provers" *)
978
  alternatives_frame c notebook;
MARCHE Claude's avatar
MARCHE Claude committed
979 980 981 982 983 984 985 986 987 988 989 990 991 992 993
  (** 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
994 995
  dialog#add_button "Close" `CLOSE ;
  let ( _ : GWindow.Buttons.about) = dialog#run () in
996 997 998 999 1000
  (* let config = set_main config *)
  (*   (set_limits (get_main config) *)
  (*      t.time_limit t.mem_limit t.max_running_processes) *)
  (* in *)

1001 1002 1003 1004
  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);
1005
  save_config ();
MARCHE Claude's avatar
MARCHE Claude committed
1006
  dialog#destroy ()
1007

1008
(*
1009
let run_auto_detection gconfig =
1010 1011
  let config = Autodetection.run_auto_detection gconfig.config in
  gconfig.config <- config;
1012 1013
  let _provers = get_provers config in
(* TODO: store the result differently
1014 1015
  gconfig.provers <- Mstr.fold (Session.get_prover_data gconfig.env) provers
  Mstr.empty
1016 1017
*)
  ()
1018
*)
MARCHE Claude's avatar
MARCHE Claude committed
1019

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

1022 1023
let uninstalled_prover c eS unknown =
  try
1024
    Whyconf.get_prover_upgrade_policy c.config unknown
1025
  with Not_found ->
1026 1027
    let others,names,versions = Session_tools.unknown_to_known_provers
      (Whyconf.get_provers eS.Session.whyconf) unknown in
1028
    let dialog = GWindow.dialog
1029
      ~icon:(!why_icon) ~modal:true
1030 1031
      ~title:"Why3: Uninstalled prover" ()
    in
1032
    let vbox = dialog#vbox in
1033
    let hb = GPack.hbox ~packing:vbox#add () in
MARCHE Claude's avatar
MARCHE Claude committed
1034
    let _ = GMisc.image ~stock:`DIALOG_WARNING ~packing:hb#add () in
1035 1036 1037 1038
    let text =
      Pp.sprintf "The prover %a is not installed"
        Whyconf.print_prover unknown
    in
MARCHE Claude's avatar
MARCHE Claude committed
1039
    let _ = GMisc.label ~ypad:20 ~text ~xalign:0.5 ~packing:hb#add () in
1040
    let label = "Please select a policy for associated proof attempts" in
1041 1042 1043 1044 1045 1046 1047 1048 1049 1050
    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"
1051
      ~active:true
1052 1053 1054 1055 1056 1057 1058 1059 1060 1061
      ~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
1062
    let alternatives_section acc label alternatives =
1063 1064 1065 1066
      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
1067
            ~packing:(vbox#pack ~fill:true ~expand:true) ()
1068 1069 1070 1071