gconfig.ml 46.8 KB
Newer Older
1 2 3
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
Guillaume Melquiond's avatar
Guillaume Melquiond committed
4
(*  Copyright 2010-2019   --   Inria - CNRS - Paris-Sud University  *)
5 6 7 8
(*                                                                  *)
(*  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.                           *)
9
(*                                                                  *)
10
(********************************************************************)
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 20 21 22 23
(** 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;
24
    (* print the stack trace if asked to (can't be done by the usual way) *)
25 26 27 28 29
    if Debug.test_flag Debug.stack_trace then
      Printf.eprintf "Backtrace:\n%t\n%!" Printexc.print_backtrace
  in
  GtkSignal.user_handler := why3_handler

30 31
(* config file *)

32
type t =
MARCHE Claude's avatar
MARCHE Claude committed
33 34 35
    { mutable window_width : int;
      mutable window_height : int;
      mutable tree_width : int;
36
      mutable task_height : int;
37
      mutable font_size : int;
38
      mutable current_tab : int;
MARCHE Claude's avatar
MARCHE Claude committed
39
      mutable verbose : int;
40
      mutable show_full_context : bool;
41
      mutable show_attributes : bool;
Mário Pereira's avatar
Mário Pereira committed
42
      mutable show_coercions : bool;
43
      mutable show_locs : bool;
MARCHE Claude's avatar
MARCHE Claude committed
44
      mutable show_time_limit : bool;
45
      mutable max_boxes : int;
46
      mutable allow_source_editing : bool;
Andrei Paskevich's avatar
Andrei Paskevich committed
47
      mutable saving_policy : int; (* 0 = always, 1 = never, 2 = ask *)
Sylvain Dailler's avatar
Sylvain Dailler committed
48
      mutable auto_next : bool; (* true if auto jump to next goal *)
Andrei Paskevich's avatar
Andrei Paskevich committed
49
      mutable premise_color : string;
50
      mutable neg_premise_color : string;
Andrei Paskevich's avatar
Andrei Paskevich committed
51
      mutable goal_color : string;
52
      mutable error_color : string;
53
      mutable error_color_bg : string;
54
      mutable error_line_color : string;
55
      mutable iconset : string;
56
      (** colors *)
57
      mutable config : Whyconf.config;
58
      original_config : Whyconf.config;
59
      (* mutable altern_provers : altern_provers; *)
60
      (* mutable replace_prover : conf_replace_prover; *)
61
      mutable hidden_provers : string list;
62 63 64
      mutable session_time_limit : int;
      mutable session_mem_limit : int;
      mutable session_nb_processes : int;
MARCHE Claude's avatar
MARCHE Claude committed
65 66
    }

MARCHE Claude's avatar
MARCHE Claude committed
67

68 69 70 71
type ide = {
  ide_window_width : int;
  ide_window_height : int;
  ide_tree_width : int;
72
  ide_task_height : int;
73
  ide_font_size : int;
74
  ide_current_tab : int;
75
  ide_verbose : int;
76
  ide_show_full_context : bool;
77
  ide_show_attributes : bool;
Mário Pereira's avatar
Mário Pereira committed
78
  ide_show_coercions : bool;
79
  ide_show_locs : bool;
MARCHE Claude's avatar
MARCHE Claude committed
80
  ide_show_time_limit : bool;
81
  ide_max_boxes : int;
82
  ide_allow_source_editing : bool;
83
  ide_saving_policy : int;
Sylvain Dailler's avatar
Sylvain Dailler committed
84
  ide_auto_next : bool;
Andrei Paskevich's avatar
Andrei Paskevich committed
85
  ide_premise_color : string;
86
  ide_neg_premise_color : string;
Andrei Paskevich's avatar
Andrei Paskevich committed
87
  ide_goal_color : string;
88
  ide_error_color : string;
89
  ide_error_color_bg : string;
90
  ide_error_line_color : string;
91
  ide_iconset : 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
let default_ide =
  { ide_window_width = 1024;
    ide_window_height = 768;
    ide_tree_width = 512;
100
    ide_task_height = 400;
101
    ide_font_size = 10;
102
    ide_current_tab = 0;
103
    ide_verbose = 0;
104
    ide_show_full_context = false;
105
    ide_show_attributes = false;
Mário Pereira's avatar
Mário Pereira committed
106
    ide_show_coercions = true;
107
    ide_show_locs = false;
MARCHE Claude's avatar
MARCHE Claude committed
108
    ide_show_time_limit = false;
MARCHE Claude's avatar
MARCHE Claude committed
109
    ide_max_boxes = 16;
110
    ide_allow_source_editing = true;
111
    ide_saving_policy = 2;
Sylvain Dailler's avatar
Sylvain Dailler committed
112
    ide_auto_next = true;
Andrei Paskevich's avatar
Andrei Paskevich committed
113
    ide_premise_color = "chartreuse";
114
    ide_neg_premise_color = "pink";
Andrei Paskevich's avatar
Andrei Paskevich committed
115
    ide_goal_color = "gold";
116
    ide_error_color_bg = "yellow";
117 118
    ide_error_color = "red";
    ide_error_line_color = "yellow";
119
    ide_iconset = "fatcow";
120
    ide_hidden_provers = [];
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";
130 131
    ide_task_height =
      get_int section ~default:default_ide.ide_task_height "task_height";
132 133
    ide_current_tab =
      get_int section ~default:default_ide.ide_current_tab "current_tab";
134 135
    ide_font_size =
      get_int section ~default:default_ide.ide_font_size "font_size";
136 137
    ide_verbose =
      get_int section ~default:default_ide.ide_verbose "verbose";
138 139 140
    ide_show_full_context =
      get_bool section ~default:default_ide.ide_show_full_context
        "show_full_context";
141 142
    ide_show_attributes =
      get_bool section ~default:default_ide.ide_show_attributes "print_attributes";
Mário Pereira's avatar
Mário Pereira committed
143
    ide_show_coercions =
144
      get_bool section ~default:default_ide.ide_show_attributes "print_coercions";
145 146
    ide_show_locs =
      get_bool section ~default:default_ide.ide_show_locs "print_locs";
MARCHE Claude's avatar
MARCHE Claude committed
147
    ide_show_time_limit =
148 149
      get_bool section ~default:default_ide.ide_show_time_limit
        "print_time_limit";
150 151 152
    ide_max_boxes =
      get_int section ~default:default_ide.ide_max_boxes
        "max_boxes";
153 154
    ide_allow_source_editing =
      get_bool section ~default:default_ide.ide_allow_source_editing "allow_source_editing";
155 156
    ide_saving_policy =
      get_int section ~default:default_ide.ide_saving_policy "saving_policy";
Sylvain Dailler's avatar
Sylvain Dailler committed
157 158
    ide_auto_next =
      get_bool section ~default:default_ide.ide_auto_next "auto_next";
Andrei Paskevich's avatar
Andrei Paskevich committed
159 160 161
    ide_premise_color =
      get_string section ~default:default_ide.ide_premise_color
        "premise_color";
162 163 164
    ide_neg_premise_color =
      get_string section ~default:default_ide.ide_neg_premise_color
        "neg_premise_color";
Andrei Paskevich's avatar
Andrei Paskevich committed
165 166 167
    ide_goal_color =
      get_string section ~default:default_ide.ide_goal_color
        "goal_color";
168 169 170
    ide_error_color =
      get_string section ~default:default_ide.ide_error_color
        "error_color";
171 172 173
    ide_error_color_bg =
      get_string section ~default:default_ide.ide_error_color_bg
        "error_color_bg";
174 175 176
    ide_error_line_color =
      get_string section ~default:default_ide.ide_error_line_color
        "error_line_color";
177
    ide_iconset =
178 179
      get_string section ~default:default_ide.ide_iconset
        "iconset";
180
    ide_hidden_provers = get_stringl ~default:default_ide.ide_hidden_provers section "hidden_prover";
181
  }
MARCHE Claude's avatar
MARCHE Claude committed
182

183

184 185
let set_attr_flag =
  let fl = Debug.lookup_flag "print_attributes" in
186 187 188
  fun b ->
    (if b then Debug.set_flag else Debug.unset_flag) fl

Mário Pereira's avatar
Mário Pereira committed
189 190 191 192 193
let set_coercions_flag =
  let fl = Debug.lookup_flag "print_coercions" in
  fun b ->
    (if b then Debug.set_flag else Debug.unset_flag) fl

194 195 196 197 198
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

Clément Fumex's avatar
Clément Fumex committed
199
let load_config config original_config =
200
  let main = get_main config in
201
  let ide  = match Whyconf.get_section config "ide" with
202
    | None -> default_ide
203 204
    | Some s -> load_ide s
  in
205
  set_attr_flag ide.ide_show_attributes;
Mário Pereira's avatar
Mário Pereira committed
206
  set_coercions_flag ide.ide_show_coercions;
207
  set_locs_flag ide.ide_show_locs;
MARCHE Claude's avatar
MARCHE Claude committed
208 209 210
  { window_height = ide.ide_window_height;
    window_width  = ide.ide_window_width;
    tree_width    = ide.ide_tree_width;
211
    task_height   = ide.ide_task_height;
212
    current_tab   = ide.ide_current_tab;
213
    font_size     = ide.ide_font_size;
MARCHE Claude's avatar
MARCHE Claude committed
214
    verbose       = ide.ide_verbose;
215
    show_full_context= ide.ide_show_full_context ;
216
    show_attributes   = ide.ide_show_attributes ;
Mário Pereira's avatar
Mário Pereira committed
217
    show_coercions = ide.ide_show_coercions ;
218
    show_locs     = ide.ide_show_locs ;
MARCHE Claude's avatar
MARCHE Claude committed
219
    show_time_limit = ide.ide_show_time_limit;
220
    max_boxes = ide.ide_max_boxes;
221
    allow_source_editing = ide.ide_allow_source_editing ;
222
    saving_policy = ide.ide_saving_policy ;
Sylvain Dailler's avatar
Sylvain Dailler committed
223
    auto_next = ide.ide_auto_next ;
Andrei Paskevich's avatar
Andrei Paskevich committed
224
    premise_color = ide.ide_premise_color;
225
    neg_premise_color = ide.ide_neg_premise_color;
Andrei Paskevich's avatar
Andrei Paskevich committed
226
    goal_color = ide.ide_goal_color;
227
    error_color = ide.ide_error_color;
228
    error_color_bg = ide.ide_error_color_bg;
229
    error_line_color = ide.ide_error_line_color;
230
    iconset = ide.ide_iconset;
MARCHE Claude's avatar
MARCHE Claude committed
231
    config         = config;
232
    original_config = original_config;
233
    hidden_provers = ide.ide_hidden_provers;
234 235 236 237
    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
238

239
let save_config t =
240
  Debug.dprintf debug "[config] saving IDE config file@.";
241
  (* taking original config, without the extra_config *)
242
  let config = t.original_config in
243 244 245 246 247
  (* 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
248 249 250 251
  let main = get_main config in
  let main = set_limits main time mem nb in
  let main = set_default_editor main (Whyconf.default_editor new_main) in
  let config = set_main config main in
252 253 254 255
  (* 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 *)
256
  let config = set_policies config (get_policies t.config) in
257 258 259 260
  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
261
  let ide = set_int ide "task_height" t.task_height in
262
  let ide = set_int ide "current_tab" t.current_tab in
263
  let ide = set_int ide "font_size" t.font_size in
264
  let ide = set_int ide "verbose" t.verbose in
265
  let ide = set_bool ide "show_full_context" t.show_full_context in
266
  let ide = set_bool ide "print_attributes" t.show_attributes in
Mário Pereira's avatar
Mário Pereira committed
267
  let ide = set_bool ide "print_coercions" t.show_coercions in
268
  let ide = set_bool ide "print_locs" t.show_locs in
MARCHE Claude's avatar
MARCHE Claude committed
269
  let ide = set_bool ide "print_time_limit" t.show_time_limit in
270
  let ide = set_int ide "max_boxes" t.max_boxes in
271
  let ide = set_bool ide "allow_source_editing" t.allow_source_editing in
272
  let ide = set_int ide "saving_policy" t.saving_policy in
Andrei Paskevich's avatar
Andrei Paskevich committed
273
  let ide = set_string ide "premise_color" t.premise_color in
274
  let ide = set_string ide "neg_premise_color" t.neg_premise_color in
Andrei Paskevich's avatar
Andrei Paskevich committed
275
  let ide = set_string ide "goal_color" t.goal_color in
276
  let ide = set_string ide "error_color" t.error_color in
277
  let ide = set_string ide "error_color_bg" t.error_color_bg in
278
  let ide = set_string ide "error_line_color" t.error_line_color in
279
  let ide = set_string ide "iconset" t.iconset in
280
  let ide = set_stringl ide "hidden_prover" t.hidden_provers in
281
  let config = Whyconf.set_section config "ide" ide in
282
  Whyconf.save_config config
MARCHE Claude's avatar
MARCHE Claude committed
283

284
let config,load_config =
285 286 287 288 289
  let config = ref None in
  (fun () ->
    match !config with
      | None -> invalid_arg "configuration not yet loaded"
      | Some conf -> conf),
Clément Fumex's avatar
Clément Fumex committed
290 291
  (fun conf base_conf ->
    let c = load_config conf base_conf in
292
    config := Some c)
293

294
let save_config () = save_config (config ())
295

296
let get_main () = (get_main (config ()).config)
297

298 299 300 301 302 303 304 305 306 307 308 309
(*


  font size


 *)


let sans_font_family = "Sans"
let mono_font_family = "Monospace"

310 311
let modifiable_sans_font_views : GObj.misc_ops list ref = ref []
let modifiable_mono_font_views : GObj.misc_ops list ref = ref []
312 313 314 315 316 317 318 319 320 321 322 323 324

let add_modifiable_sans_font_view v =
  modifiable_sans_font_views := v :: !modifiable_sans_font_views

let add_modifiable_mono_font_view v =
  modifiable_mono_font_views := v :: !modifiable_mono_font_views

let change_font size =
(*
  Tools.resize_images (!Colors.font_size * 2 - 4);
*)
  let sff = sans_font_family ^ " " ^ string_of_int size in
  let mff = mono_font_family ^ " " ^ string_of_int size in
325 326
  let sf = Gtkcompat.gpango_font_description_from_string sff in
  let mf = Gtkcompat.gpango_font_description_from_string mff in
327 328 329
  List.iter (fun v -> v#modify_font sf) !modifiable_sans_font_views;
  List.iter (fun v -> v#modify_font mf) !modifiable_mono_font_views

330 331 332 333 334
let incr_font_size n =
  let c = config () in
  let s = max (c.font_size + n) 4 in
  c.font_size <- s;
  s
335

Clément Fumex's avatar
Clément Fumex committed
336
let enlarge_fonts () = change_font (incr_font_size 1)
337

Clément Fumex's avatar
Clément Fumex committed
338
let reduce_fonts () = change_font (incr_font_size (-1))
339

Clément Fumex's avatar
Clément Fumex committed
340
let set_fonts () = change_font (incr_font_size 0)
341

MARCHE Claude's avatar
MARCHE Claude committed
342 343
(*

MARCHE Claude's avatar
MARCHE Claude committed
344
  images, icons
MARCHE Claude's avatar
MARCHE Claude committed
345 346 347

*)

François Bobot's avatar
François Bobot committed
348
let image_default = ref (GdkPixbuf.create ~width:1 ~height:1 ())
349
(* dumb pixbuf *)
350
let image_undone = ref !image_default
MARCHE Claude's avatar
MARCHE Claude committed
351 352 353 354 355 356
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
357
let image_outofmemory = ref !image_default
358
let image_steplimitexceeded = ref !image_default
MARCHE Claude's avatar
MARCHE Claude committed
359
let image_failure = ref !image_default
360 361 362 363
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
364
let image_outofmemory_obs = ref !image_default
365
let image_steplimitexceeded_obs = ref !image_default
366
let image_failure_obs = ref !image_default
MARCHE Claude's avatar
MARCHE Claude committed
367 368 369
let image_yes = ref !image_default
let image_no = ref !image_default
let image_file = ref !image_default
370 371
let image_theory = ref !image_default
let image_goal = ref !image_default
MARCHE Claude's avatar
MARCHE Claude committed
372 373
let image_prover = ref !image_default
let image_transf = ref !image_default
374
let image_metas = ref !image_default
MARCHE Claude's avatar
MARCHE Claude committed
375
let image_editor = ref !image_default
376
let image_replay = ref !image_default
377
let image_cancel = ref !image_default
MARCHE Claude's avatar
MARCHE Claude committed
378
let image_reload = ref !image_default
MARCHE Claude's avatar
MARCHE Claude committed
379
let image_remove = ref !image_default
380
let image_cleaning = ref !image_default
MARCHE Claude's avatar
MARCHE Claude committed
381

MARCHE Claude's avatar
MARCHE Claude committed
382 383
let why_icon = ref !image_default

384 385
let image ?size f =
  let main = get_main () in
386
  let n =
387 388 389
    Filename.concat (datadir main)
      (Filename.concat "images" (f^".png"))
  in
390
  try (
391 392 393 394 395
  match size with
    | None ->
        GdkPixbuf.from_file n
    | Some s ->
        GdkPixbuf.from_file_at_size ~width:s ~height:s n
396
  ) with _ -> !image_default
397 398 399 400 401 402 403 404 405 406

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 ""
407
let iconname_steplimitexceeded = ref ""
408 409 410 411 412 413
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 ""
414
let iconname_steplimitexceeded_obs = ref ""
415 416 417 418
let iconname_failure_obs = ref ""
let iconname_yes = ref ""
let iconname_no = ref ""
let iconname_file = ref ""
419 420
let iconname_theory = ref ""
let iconname_goal = ref ""
421 422
let iconname_prover = ref ""
let iconname_transf = ref ""
423
let iconname_metas  = ref ""
424 425 426 427 428 429 430
let iconname_editor = ref ""
let iconname_replay = ref ""
let iconname_cancel = ref ""
let iconname_reload = ref ""
let iconname_remove = ref ""
let iconname_cleaning = ref ""

431
let iconsets () : (string * Why3.Rc.family) =
432
  let main = get_main () in
433
  let dir = Filename.concat (datadir main) "images" in
434 435 436 437 438 439 440 441 442 443
  let files = Sys.readdir dir in
  let f = ref [] in
  Array.iter
    (fun fn ->
       if Filename.check_suffix fn ".rc" then
         let n = Filename.concat dir fn in
         let d = Rc.from_file n in
         f := List.rev_append (Rc.get_family d "iconset") !f)
    files;
  (dir, !f)
444 445 446 447

let load_icon_names () =
  let ide = config () in
  let iconset = ide.iconset in
448
  let _,iconsets = iconsets () in
449
  let iconset,d =
450
    try
451
      iconset, List.assoc iconset iconsets
452 453
    with Not_found ->
      try
454
        "fatcow", List.assoc "fatcow" iconsets
455 456 457
      with Not_found ->
        failwith "No icon set found"
  in
458 459 460 461 462 463 464 465 466 467 468 469
  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";
470
  iconname_steplimitexceeded := get_icon_name "steplimitexceeded";
471 472 473 474 475 476
  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";
477
  iconname_steplimitexceeded_obs := get_icon_name "steplimitexceeded_obs";
478 479 480 481 482 483 484 485
  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";
486
  iconname_metas  := get_icon_name "metas";
487 488 489 490 491 492
  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";
493 494
  ()

MARCHE Claude's avatar
MARCHE Claude committed
495
let resize_images size =
496 497 498 499 500 501 502 503 504
  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;
505
  image_steplimitexceeded := image ~size !iconname_steplimitexceeded;
506 507 508 509 510 511
  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;
512
  image_steplimitexceeded_obs := image ~size !iconname_steplimitexceeded_obs;
513 514 515 516
  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;
517 518
  image_theory := image ~size !iconname_theory;
  image_goal := image ~size !iconname_goal;
519 520
  image_prover := image ~size !iconname_prover;
  image_transf := image ~size !iconname_transf;
521
  image_metas := image ~size !iconname_metas;
522 523 524 525 526 527
  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
528 529
  ()

530
let init () =
531
  Debug.dprintf debug "[config] reading icons...@?";
532
  load_icon_names ();
MARCHE Claude's avatar
MARCHE Claude committed
533
  why_icon := image "logo-why";
MARCHE Claude's avatar
MARCHE Claude committed
534
  resize_images 20;
535
  Debug.dprintf debug " done.@."
MARCHE Claude's avatar
MARCHE Claude committed
536

537
let show_legend_window ~parent () =
538 539
  let dialog =
    GWindow.dialog
540
      ~modal:true ~parent
541 542 543
      ~title:"Why3: legend of icons" ~icon:!why_icon
      ()
  in
MARCHE Claude's avatar
MARCHE Claude committed
544
  let vbox = dialog#vbox in
545 546
  let text = GText.view ~packing:vbox#add
    ~editable:false ~cursor_visible:false () in
MARCHE Claude's avatar
MARCHE Claude committed
547
  let b = text#buffer in
548 549
  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
550
  let i s = b#insert ~iter:b#end_iter s in
551
  let it s = b#insert ~iter:b#end_iter ~tags:[tt] s in
MARCHE Claude's avatar
MARCHE Claude committed
552
  let ib i = b#insert_pixbuf ~iter:b#end_iter ~pixbuf:!i in
553
  it "Tree view\n";
MARCHE Claude's avatar
MARCHE Claude committed
554
  ib image_file;
555 556 557 558
  i "   File, containing a set of theories\n";
  ib image_theory;
  i "   Theory, containing a set of goals\n";
  ib image_goal;
559
  i "   Goal\n";
MARCHE Claude's avatar
MARCHE Claude committed
560
  ib image_prover;
561
  i "   External prover\n";
MARCHE Claude's avatar
MARCHE Claude committed
562
  ib image_transf;
563
  i "   Transformation or strategy\n";
564
  it "Status column\n";
565 566
  ib image_undone;
  i "   External proof attempt not done\n";
MARCHE Claude's avatar
MARCHE Claude committed
567
  ib image_scheduled;
568
  i "   Scheduled external proof attempt\n";
MARCHE Claude's avatar
MARCHE Claude committed
569
  ib image_running;
570
  i "   Running external proof attempt\n";
MARCHE Claude's avatar
MARCHE Claude committed
571
  ib image_valid;
572 573 574
  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
575
  ib image_timeout;
576
  i "   External prover reached the time limit\n";
577 578
  ib image_outofmemory;
  i "   External prover ran out of memory\n";
579 580
  ib image_steplimitexceeded;
  i "   External prover exceeded the step limit\n";
MARCHE Claude's avatar
MARCHE Claude committed
581
  ib image_unknown;
582
  i "   External prover answer not conclusive\n";
MARCHE Claude's avatar
MARCHE Claude committed
583
  ib image_failure;
584
  i "   External prover call failed\n";
585 586 587 588
  ib image_valid_obs;
  i "   Valid but obsolete result\n";
  ib image_unknown_obs;
  i "   Answer not conclusive and obsolete\n";
589 590 591 592 593 594
  ib image_timeout_obs;
  i "   Time limit reached, obsolete\n";
  ib image_outofmemory_obs;
  i "   Out of memory, obsolete\n";
  ib image_steplimitexceeded_obs;
  i "   Step limit exceeded, obsolete\n";
595 596 597 598
  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
599
  dialog#add_button "Close" `CLOSE ;
600 601
  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
602 603 604 605
  let ( _ : GWindow.Buttons.about) = dialog#run () in
  dialog#destroy ()


606
let show_about_window ~parent () =
MARCHE Claude's avatar
MARCHE Claude committed
607 608
  let about_dialog =
    GWindow.about_dialog
609
      ~parent
Guillaume Melquiond's avatar
Guillaume Melquiond committed
610
      ~name:"The Why3 Verification Platform"
611 612 613
      ~authors:["François Bobot";
                "Jean-Christophe Filliâtre";
                "Claude Marché";
614 615 616 617 618
                "Guillaume Melquiond";
                "Andrei Paskevich";
                "";
                "with contributions of";
                "";
619
                "Stefan Berghofer";
620
                "Sylvie Boldo";
621
                "Martin Clochard";
622
                "Simon Cruanes";
MARCHE Claude's avatar
MARCHE Claude committed
623
                "Sylvain Dailler";
624
                "Clément Fumex";
625
                "Léon Gondelman";
626
                "David Hauzar";
627
                "Daisuke Ishii";
628
                "Johannes Kanig";
MARCHE Claude's avatar
MARCHE Claude committed
629
                "Mikhail Mandrykin";
630 631
                "David Mentré";
                "Benjamin Monate";
Guillaume Melquiond's avatar
Guillaume Melquiond committed
632
                "Kim Nguyễn";
633
                "Thi-Minh-Tuyen Nguyen";
634 635
                "Mário Pereira";
                "Raphaël Rieu-Helft";
636
                "Simão Melo de Sousa";
637 638 639
                "Asma Tafat";
                "Piotr Trojanek";
                "Makarius Wenzel";
MARCHE Claude's avatar
MARCHE Claude committed
640
               ]
Guillaume Melquiond's avatar
Guillaume Melquiond committed
641
      ~copyright:"Copyright 2010-2019 Inria, CNRS, Paris-Sud University"
642
      ~license:("See file " ^ Filename.concat Config.datadir "LICENSE")
Guillaume Melquiond's avatar
Guillaume Melquiond committed
643 644
      ~website:"http://why3.lri.fr/"
      ~website_label:"http://why3.lri.fr/"
645
      ~version:Config.version
Guillaume Melquiond's avatar
Guillaume Melquiond committed
646 647
      ~icon:!why_icon
      ~logo:!why_icon
MARCHE Claude's avatar
MARCHE Claude committed
648
      ()
MARCHE Claude's avatar
MARCHE Claude committed
649
  in
MARCHE Claude's avatar
MARCHE Claude committed
650 651
  let ( _ : GWindow.Buttons.about) = about_dialog#run () in
  about_dialog#destroy ()
MARCHE Claude's avatar
MARCHE Claude committed
652

653

654

655 656 657

(**** Preferences Window ***)

658
let general_settings (c : t) (notebook:GPack.notebook) =
659 660
  let label = GMisc.label ~text:"General" () in
  let page =
MARCHE Claude's avatar
MARCHE Claude committed
661
    GPack.vbox ~homogeneous:false ~packing:
662
      (fun w -> ignore(notebook#append_page ~tab_label:label#coerce w)) ()
663
  in
664
  (* debug mode ? *)
665
(*
MARCHE Claude's avatar
MARCHE Claude committed
666
  let debugmode =
MARCHE Claude's avatar
MARCHE Claude committed
667
    GButton.check_button ~label:"debug" ~packing:page1#add ()
MARCHE Claude's avatar
MARCHE Claude committed
668 669
      ~active:(c.verbose > 0)
  in
MARCHE Claude's avatar
MARCHE Claude committed
670
  let (_ : GtkSignal.id) =
MARCHE Claude's avatar
MARCHE Claude committed
671 672
    debugmode#connect#toggled ~callback:
      (fun () -> c.verbose <- 1 - c.verbose)
MARCHE Claude's avatar
MARCHE Claude committed
673
  in
674
*)
675
  let page_pack = page#pack ?from:None ?expand:None ?fill:None ?padding:None in
676
  let external_processes_options_frame =
677
    GBin.frame ~label:"External provers options" ~packing:page_pack ()
678 679 680 681
  in
  let vb = GPack.vbox ~homogeneous:false
    ~packing:external_processes_options_frame#add ()
  in
682
  (* time limit *)
683 684 685
  let width = 300 and xalign = 0.0 in
  let hb = GPack.hbox ~homogeneous:false ~packing:vb#add () in
  let hb_pack = hb#pack ~expand:false ?from:None ?fill:None ?padding:None in
686
  let _ = GMisc.label ~text:"Time limit (in sec.): " ~width ~xalign
687
    ~packing:hb_pack () in
688
  let timelimit_spin = GEdit.spin_button ~digits:0 ~packing:hb#add () in
689
  timelimit_spin#adjustment#set_bounds ~lower:0. ~upper:86_400. ~step_incr:5. ();
690
  timelimit_spin#adjustment#set_value (float_of_int c.session_time_limit);
MARCHE Claude's avatar
MARCHE Claude committed
691
  let (_ : GtkSignal.id) =
692
    timelimit_spin#connect#value_changed ~callback:
693
      (fun () -> c.session_time_limit <- timelimit_spin#value_as_int)
694
  in
695
  (* mem limit *)
696 697
  let hb = GPack.hbox ~homogeneous:false ~packing:vb#add () in
  let hb_pack = hb#pack ~expand:false ?from:None ?fill:None ?padding:None in
698
  let _ = GMisc.label ~text:"Memory limit (in Mb): " ~width ~xalign
699
    ~packing:hb_pack () in
700
  let memlimit_spin = GEdit.spin_button ~digits:0 ~packing:hb#add () in
701
  memlimit_spin#adjustment#set_bounds ~lower:0. ~upper:16_000. ~step_incr:500. ();
702
  memlimit_spin#adjustment#set_value (float_of_int c.session_mem_limit);
703 704
  let (_ : GtkSignal.id) =
    memlimit_spin#connect#value_changed ~callback:
705 706 707
      (fun () -> c.session_mem_limit <- memlimit_spin#value_as_int)
  in
  (* nb of processes *)
708 709
  let hb = GPack.hbox ~homogeneous:false ~packing:vb#add () in
  let hb_pack = hb#pack ~expand:false ?from:None ?fill:None ?padding:None in
710
  let _ = GMisc.label ~text:"Nb of processes: " ~width ~xalign
711
    ~packing:hb_pack () in
MARCHE Claude's avatar
MARCHE Claude committed
712
  let nb_processes_spin = GEdit.spin_button ~digits:0 ~packing:hb#add () in
713
  nb_processes_spin#adjustment#set_bounds
714
    ~lower:1. ~upper:64. ~step_incr:1. ();
715
  nb_processes_spin#adjustment#set_value
716
    (float_of_int c.session_nb_processes);
MARCHE Claude's avatar
MARCHE Claude committed
717
  let (_ : GtkSignal.id) =
MARCHE Claude's avatar
MARCHE Claude committed
718
    nb_processes_spin#connect#value_changed ~callback:
719 720
      (fun () -> c.session_nb_processes <- nb_processes_spin#value_as_int)
  in
721
  (* counter-example *)
722
(*
723 724 725 726 727 728 729 730
  let cntexample_check = GButton.check_button ~label:"get counter-example"
    ~packing:vb#add ()
    ~active:c.session_cntexample
  in
  let (_: GtkSignal.id) =
    cntexample_check#connect#toggled ~callback:
      (fun () -> c.session_cntexample <- not c.session_cntexample)
  in
731
*)
732 733 734 735 736 737 738 739 740
  (* source editing allowed *)
  let source_editing_check = GButton.check_button ~label:"allow editing source files"
    ~packing:vb#add ()
    ~active:c.allow_source_editing
  in
  let (_: GtkSignal.id) =
    source_editing_check#connect#toggled ~callback:
      (fun () -> c.allow_source_editing <- not c.allow_source_editing)
  in
Sylvain Dailler's avatar
Sylvain Dailler committed
741 742 743 744 745 746 747 748 749 750
  (* Auto jump to next unproved goals *)
  let auto_next_check = GButton.check_button
      ~label:"Allow auto jumping to next unproved goal"
      ~packing:vb#add ()
      ~active:c.auto_next
  in
  let (_: GtkSignal.id) =
    auto_next_check#connect#toggled ~callback:
      (fun () -> c.auto_next <- not c.auto_next)
  in
751 752 753 754 755 756 757 758 759 760 761 762 763 764 765 766 767 768 769 770 771 772 773 774 775 776 777 778 779 780 781 782 783 784 785 786 787 788 789 790 791 792 793 794 795 796 797 798 799 800 801 802 803 804 805
  (* session saving policy *)
  let set_saving_policy n () = c.saving_policy <- n in
  let saving_policy_frame =
    GBin.frame ~label:"Session saving policy"
      ~packing:page_pack ()
  in
  let saving_policy_box =
    GPack.button_box
      `VERTICAL ~border_width:5 ~spacing:5
      ~packing:saving_policy_frame#add ()
  in
  let saving_policy_box_pack =
    saving_policy_box#pack ?from:None ?expand:None ?fill:None ?padding:None
  in
  let choice0 =
    GButton.radio_button
      ~label:"always save on exit"
      ~active:(c.saving_policy = 0)
      ~packing:saving_policy_box_pack ()
  in
  let choice1 =
    GButton.radio_button
      ~label:"never save on exit" ~group:choice0#group
      ~active:(c.saving_policy = 1)
      ~packing:saving_policy_box_pack ()
  in
  let choice2 =
    GButton.radio_button
      ~label:"ask whether to save on exit" ~group:choice0#group
      ~active:(c.saving_policy = 2)
      ~packing:saving_policy_box_pack ()
  in
  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
  let (_ : GPack.box) =
    GPack.vbox ~packing:page_pack ()
  in
  ()

(** Appearance *)

let appearance_settings (c : t) (notebook:GPack.notebook) =
  let label = GMisc.label ~text:"Appearance" () in
  let page =
    GPack.vbox ~homogeneous:false ~packing:
      (fun w -> ignore(notebook#append_page ~tab_label:label#coerce w)) ()
  in
  let page_pack = page#pack ?from:None ?expand:None ?fill:None ?padding:None in
806
  let display_options_frame =
807
    GBin.frame ~label:"Display options" ~packing:page_pack ()
808
  in
809 810
  let vb = GPack.vbox ~homogeneous:false
    ~packing:display_options_frame#add ()
811
  in
812
  (* max boxes *)
813 814
  let width = 300 and xalign = 0.0 in
  let hb = GPack.hbox ~homogeneous:false ~packing:vb#add () in
815
  let hb_pack = hb#pack ~expand:false ?fill:None ?from:None ?padding:None in
816
  let _ = GMisc.label ~text:"Use ellipsis for terms deeper than: " ~width ~xalign ~packing:hb_pack () in
817 818 819 820 821 822 823
  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
824 825 826 827 828
  (* options for task display *)
  let display_options_box =
    GPack.button_box `VERTICAL ~border_width:5 ~spacing:5
      ~packing:vb#add ()
  in
829 830 831 832 833 834 835 836 837
  let showfullcontext =
    GButton.check_button ~label:"show full task context"
      ~packing:display_options_box#add ()
      ~active:c.show_full_context
  in
  let (_ : GtkSignal.id) =
    showfullcontext#connect#toggled ~callback:
      (fun () -> c.show_full_context <- not c.show_full_context)
  in
838
  let showattrs =
839
    GButton.check_button
840
      ~label:"show attributes in formulas"
841
      ~packing:display_options_box#add ()
842
      ~active:c.show_attributes
843 844
  in
  let (_ : GtkSignal.id) =
845
    showattrs#connect#toggled ~callback:
846
      (fun () ->
847 848
         c.show_attributes <- not c.show_attributes;
         set_attr_flag c.show_attributes)
849
  in
Mário Pereira's avatar
Mário Pereira committed
850 851 852 853 854 855 856 857 858 859 860 861
  let showcoercions =
    GButton.check_button
      ~label:"show coercions in formulas"
      ~packing:display_options_box#add ()
      ~active:c.show_coercions
  in
  let (_ : GtkSignal.id) =
    showcoercions#connect#toggled ~callback:
      (fun () ->
         c.show_coercions <- not c.show_coercions;
         set_coercions_flag c.show_coercions)
  in
862
  let showlocs =
863 864
    GButton.check_button
      ~label:"show source locations in formulas"
865
      ~packing:display_options_box#add ()
866
      ~active:c.show_locs
867 868 869
  in
  let (_ : GtkSignal.id) =
    showlocs#connect#toggled ~callback:
870 871
      (fun () ->
         c.show_locs <- not c.show_locs;
872 873
         set_locs_flag c.show_locs)
  in
MARCHE Claude's avatar
MARCHE Claude committed
874 875
  let showtimelimit =
    GButton.check_button
876
      ~label:"show time and memory limits for each proof"
MARCHE Claude's avatar
MARCHE Claude committed
877 878 879 880 881 882 883 884
      ~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
885 886 887
  (* icon sets *)
  let icon_sets_frame =
    GBin.frame ~label:"Change icon family (needs save & restart)"
888
      ~packing:page_pack ()
889
  in
890
  let icon_sets_box =
891 892
    GPack.button_box
      `VERTICAL ~border_width:5 ~spacing:5
893 894 895 896 897
      ~packing:icon_sets_frame#add ()
  in
  let icon_sets_box_pack =
    icon_sets_box#pack ?from:None ?expand:None ?fill:None ?padding:None
  in
898
  let dir,iconsets = iconsets () in
899 900
  let set_icon_set s () = c.iconset <- s in
  let (_,choices) = List.fold_left
901 902 903 904 905 906 907 908 909 910 911 912 913 914 915 916 917 918 919 920 921 922 923 924 925 926 927 928 929 930 931 932 933 934 935 936 937 938
    (fun (acc,l) (s,fields) ->
      let name = Rc.get_string ~default:s fields "name" in
      let license = Rc.get_string ~default:"" fields "license" in
      let acc,choice =
        match acc with
        | None ->
          let choice =
            GButton.radio_button
              ~label:name
              ~active:(c.iconset = s)
              ~packing:icon_sets_box_pack ()
          in
          (Some choice,choice)
        | Some c0 ->
          let choice =
            GButton.radio_button
              ~label:name
              ~active:(c.iconset = s)
              ~group:c0#group
              ~packing:icon_sets_box_pack ()
          in (acc,choice)
      in
      if license <> "" then
        begin
          let f = Filename.concat (Filename.concat dir s) license in
          let c = Sysutil.file_contents f in
          let text = "See license in " ^ f ^ ":\n\n" in
          let l = String.length c in
          let text =
            if l >= 256 then
              text ^ String.sub c 0 255 ^ "\n[...]"
            else
              text ^ c
          in
          choice#misc#set_tooltip_markup text
        end;
      (acc,(s,choice)::l))
    (None,[]) iconsets
939 940 941 942 943 944 945
  in
  List.iter
    (fun (s,c) ->
      let (_ : GtkSignal.id) =
        c#connect#toggled ~callback:(set_icon_set s)
      in ())
    choices;
946
  let (_ : GPack.box) =
947
    GPack.vbox ~packing:page_pack ()
948
  in
949
  ()
950 951

(* Page "Provers" *)
Clément Fumex's avatar
Clément Fumex committed
952

953 954 955 956 957 958
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
959 960 961
  let page_pack = page#pack ~fill:true ~expand:true ?from:None ?padding:None in
  let hbox = GPack.hbox ~packing:page_pack () in
  let hbox_pack = hbox#pack ~fill:true ~expand:true ?from:None ?padding:None in
962 963 964
  let scrollview =
  try
    GBin.scrolled_window ~hpolicy:`NEVER ~vpolicy:`AUTOMATIC
965
      ~packing:hbox_pack ()
966 967 968
  with Gtk.Error _ -> assert false
  in let () = scrollview#set_shadow_type `OUT in
  let vbox = GPack.vbox ~packing:scrollview#add_with_viewport () in
969 970 971
  let vbox_pack = vbox#pack ~fill:true ~expand:true ?from:None ?padding:None in
  let hbox = GPack.hbox ~packing:vbox_pack () in
  let hbox_pack = hbox#pack ~fill:true ~expand:true ?from:None ?padding:None in
972
  (* show/hide provers *)
973
  let frame =
974
    GBin.frame ~label:"Provers visible in the context menu" ~packing:hbox_pack ()
975
  in
976 977
  let provers_box =
    GPack.button_box `VERTICAL ~border_width:5 ~spacing:5
978
      ~packing:frame#add () in
979 980 981
  let hidden_provers = Hashtbl.create 7 in
  Mprover.iter
    (fun _ p ->
982 983 984 985
      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;
986 987 988 989 990 991 992 993 994 995 996
      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 ())
997 998
    (Whyconf.get_provers c.config);
  (* default prover *)
999
(*
1000
  let frame2 =
1001
    GBin.frame ~label:"Default prover" ~packing:hbox_pack () in
1002 1003 1004
  let provers_box =
    GPack.button_box `VERTICAL ~border_width:5 ~spacing:5
      ~packing:frame2#add () in
1005 1006 1007
  let group =
    let b =
      GButton.radio_button ~label:"(none)" ~packing:provers_box#add
1008
                           ~active:(c.config.default_prover = "") () in
1009
    let (_ : GtkSignal.id) =
1010
      b#connect#toggled ~callback:(fun () -> c.config.default_prover <- "") in
1011
    b#group in
1012 1013 1014 1015 1016
  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 =
1017
        GButton.radio_button ~label ~group ~packing:provers_box#add
1018
                             ~active:(name = c.config.default_prover) () in
1019
      let (_ : GtkSignal.id) =
1020
        b#connect#toggled ~callback:(fun () -> c.config.default_prover <- name)
1021
      in ())
1022
    (Whyconf.get_provers c.config)
1023 1024
 *)
  ()
1025

1026 1027 1028
(* Page "Uninstalled provers" *)

let alternatives_frame c (notebook:GPack.notebook) =
1029
  let label = GMisc.label ~text:"Uninstalled provers policies" () in
1030 1031 1032 1033
  let page =
    GPack.vbox ~homogeneous:false ~packing:
      (fun w -> ignore(notebook#append_page ~tab_label:label#coerce w)) ()
  in
1034
  let page_pack = page#pack ?fill:None ?expand:None ?from:None ?padding:None in
1035
  let frame =
1036
    GBin.frame ~label:"Click to remove a setting" ~packing:page_pack ()
1037 1038 1039 1040 1041 1042 1043
  in
  let box =
    GPack.button_box `VERTICAL ~border_width:5 ~spacing:5
      ~packing:frame#add ()
  in
  let remove button p () =
    button#destroy ();
1044
    c.config <- set_policies c.config (Mprover.remove p (get_policies c.config));
1045 1046 1047 1048
  in
  let iter p policy =
    let label =
      match policy with
1049
        | CPU_remove -> Pp.sprintf_wnl "proofs with %a removed" print_prover p
1050 1051 1052 1053 1054 1055 1056 1057 1058 1059 1060 1061
        | 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);
1062 1063
  let page_pack = page#pack ?fill:None ~expand:true ?from:None ?padding:None in
  let _fillbox = GPack.vbox ~packing:page_pack () in
1064 1065 1066 1067 1068 1069 1070 1071
  ()

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
1072 1073 1074
  let page_pack = page#pack ~fill:true ~expand:true ?from:None ?padding:None in
  let hbox = GPack.hbox ~packing:page_pack () in
  let hbox_pack = hbox#pack ~fill:true ~expand:true ?from:None ?padding:None in
1075 1076
  let scrollview =
    GBin.scrolled_window ~hpolicy:`NEVER ~vpolicy:`AUTOMATIC
1077
      ~packing:hbox_pack ()
1078 1079
  in
  let vbox = GPack.vbox ~packing:scrollview#add_with_viewport () in
1080
  let vbox_pack = vbox#pack ?fill:None ?expand:None ?from:None ?padding:None in
1081
  let default_editor_frame =
1082
    GBin.frame ~label:"Default editor" ~packing:vbox_pack ()
1083
  in
1084
  let main = Whyconf.get_main c.config in
1085
  let editor_entry =
1086
   GEdit.entry ~text:(default_editor main) ~packing:default_editor_frame#add ()
1087 1088
  in
  let (_ : GtkSignal.id) =
1089 1090 1091 1092 1093
    editor_entry#connect#changed
      ~callback:
      (fun () ->
       c.config <- Whyconf.set_main c.config
	(Whyconf.set_default_editor main editor_entry#text))
1094
  in
1095
  let frame = GBin.frame ~label:"Specific editors" ~packing:vbox_pack () in
1096
  let box = GPack.vbox ~border_width:5 ~packing:frame#add () in
1097
  let box_pack = box#pack ?fill:None ?expand:None ?from:None ?padding:None in
1098
  let editors = Whyconf.get_editors c.config in
MARCHE Claude's avatar
MARCHE Claude committed
1099
  let _,strings,indexes,map =
1100
    Meditor.fold
1101
      (fun k data (i,str,ind,map) ->
MARCHE Claude's avatar
MARCHE Claude committed
1102 1103 1104
        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)
1105
  in
MARCHE Claude's avatar
MARCHE Claude committed
1106
  let strings = "(default)" :: "--" :: (List.rev strings) in
1107
  let add_prover p pi =
1108
    let text = Pp.string_of_wnl Whyconf.print_prover p in
1109 1110 1111 1112 1113
    let hb = GPack.hbox ~homogeneous:false ~packing:box_pack () in
    let hb_pack_fill_expand =
      hb#pack ~fill:true ~expand:true ?from:None ?padding:None
    in
    let hb_pack = hb#pack ?fill:None ?expand:None ?from:None ?padding:None in
1114
    let _ = GMisc.label ~width:150 ~xalign:0.0 ~text
1115
      ~packing:hb_pack_fill_expand () in
1116
    let (combo, ((_ : GTree.list_store), column)) =