gconfig.ml 42.1 KB
Newer Older
Andrei Paskevich's avatar
Andrei Paskevich committed
1 2 3
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
Andrei Paskevich's avatar
Andrei Paskevich committed
4
(*  Copyright 2010-2016   --   INRIA - CNRS - Paris-Sud University  *)
Andrei Paskevich's avatar
Andrei Paskevich committed
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
(*                                                                  *)
Andrei Paskevich's avatar
Andrei Paskevich committed
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 font_size : int;
37
      mutable current_tab : int;
MARCHE Claude's avatar
MARCHE Claude committed
38
      mutable verbose : int;
39
      mutable default_prover : string; (* "" means none *)
40
      mutable default_editor : string;
41
      mutable intro_premises : bool;
MARCHE Claude's avatar
MARCHE Claude committed
42
      mutable show_labels : bool;
43
      mutable show_locs : bool;
MARCHE Claude's avatar
MARCHE Claude committed
44
      mutable show_time_limit : bool;
MARCHE Claude's avatar
MARCHE Claude committed
45
      mutable max_boxes : int;
46
      mutable saving_policy : int;
47
      (** 0 = always, 1 = never, 2 = ask *)
Andrei Paskevich's avatar
minor  
Andrei Paskevich committed
48
      mutable premise_color : string;
49
      mutable neg_premise_color : string;
Andrei Paskevich's avatar
minor  
Andrei Paskevich committed
50
      mutable goal_color : string;
51
      mutable error_color : string;
MARCHE Claude's avatar
MARCHE Claude committed
52
      mutable iconset : string;
53
      (** colors *)
MARCHE Claude's avatar
MARCHE Claude committed
54
      mutable env : Env.env;
55
      mutable config : Whyconf.config;
56
      original_config : Whyconf.config;
57
      (* mutable altern_provers : altern_provers; *)
58
      (* mutable replace_prover : conf_replace_prover; *)
59 60
      (* hidden prover buttons *)
      mutable hidden_provers : string list;
61 62 63
      mutable session_time_limit : int;
      mutable session_mem_limit : int;
      mutable session_nb_processes : int;
64
      mutable session_cntexample : bool;
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_font_size : int;
73
  ide_current_tab : int;
74
  ide_verbose : int;
75 76 77
  ide_intro_premises : bool;
  ide_show_labels : bool;
  ide_show_locs : bool;
MARCHE Claude's avatar
MARCHE Claude committed
78
  ide_show_time_limit : bool;
MARCHE Claude's avatar
MARCHE Claude committed
79
  ide_max_boxes : int;
80
  ide_saving_policy : int;
Andrei Paskevich's avatar
minor  
Andrei Paskevich committed
81
  ide_premise_color : string;
82
  ide_neg_premise_color : string;
Andrei Paskevich's avatar
minor  
Andrei Paskevich committed
83
  ide_goal_color : string;
84
  ide_error_color : string;
MARCHE Claude's avatar
MARCHE Claude committed
85
  ide_iconset : string;
86
  ide_default_prover : string;
87
  ide_default_editor : string;
88
  (* ide_replace_prover : conf_replace_prover; *)
89
  ide_hidden_provers : string list;
90
}
MARCHE Claude's avatar
MARCHE Claude committed
91

92 93 94 95
let default_ide =
  { ide_window_width = 1024;
    ide_window_height = 768;
    ide_tree_width = 512;
96
    ide_font_size = 10;
97
    ide_current_tab = 0;
98
    ide_verbose = 0;
99 100 101
    ide_intro_premises = true;
    ide_show_labels = false;
    ide_show_locs = false;
MARCHE Claude's avatar
MARCHE Claude committed
102
    ide_show_time_limit = false;
MARCHE Claude's avatar
MARCHE Claude committed
103
    ide_max_boxes = 16;
104
    ide_saving_policy = 2;
Andrei Paskevich's avatar
minor  
Andrei Paskevich committed
105
    ide_premise_color = "chartreuse";
106
    ide_neg_premise_color = "pink";
Andrei Paskevich's avatar
minor  
Andrei Paskevich committed
107
    ide_goal_color = "gold";
108
    ide_error_color = "orange";
MARCHE Claude's avatar
MARCHE Claude committed
109
    ide_iconset = "fatcow";
110
    ide_default_prover = "";
111
    ide_default_editor =
112 113 114
      (try Sys.getenv "EDITOR" ^ " %f"
       with Not_found -> "editor %f");
    ide_hidden_provers = [];
115 116 117 118 119 120 121 122 123
  }

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";
124 125
    ide_current_tab =
      get_int section ~default:default_ide.ide_current_tab "current_tab";
126 127
    ide_font_size =
      get_int section ~default:default_ide.ide_font_size "font_size";
128 129
    ide_verbose =
      get_int section ~default:default_ide.ide_verbose "verbose";
130
    ide_intro_premises =
François Bobot's avatar
François Bobot committed
131 132
      get_bool section ~default:default_ide.ide_intro_premises
        "intro_premises";
133 134 135 136
    ide_show_labels =
      get_bool section ~default:default_ide.ide_show_labels "print_labels";
    ide_show_locs =
      get_bool section ~default:default_ide.ide_show_locs "print_locs";
MARCHE Claude's avatar
MARCHE Claude committed
137
    ide_show_time_limit =
138 139
      get_bool section ~default:default_ide.ide_show_time_limit
        "print_time_limit";
MARCHE Claude's avatar
MARCHE Claude committed
140 141 142
    ide_max_boxes =
      get_int section ~default:default_ide.ide_max_boxes
        "max_boxes";
143 144
    ide_saving_policy =
      get_int section ~default:default_ide.ide_saving_policy "saving_policy";
Andrei Paskevich's avatar
minor  
Andrei Paskevich committed
145 146 147
    ide_premise_color =
      get_string section ~default:default_ide.ide_premise_color
        "premise_color";
148 149 150
    ide_neg_premise_color =
      get_string section ~default:default_ide.ide_neg_premise_color
        "neg_premise_color";
Andrei Paskevich's avatar
minor  
Andrei Paskevich committed
151 152 153
    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
    ide_hidden_provers = get_stringl ~default:default_ide.ide_hidden_provers section "hidden_prover";
167
  }
MARCHE Claude's avatar
MARCHE Claude committed
168

169 170 171 172 173 174 175 176 177 178 179

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

180
let load_config config original_config env =
Andrei Paskevich's avatar
Andrei Paskevich committed
181
  let main = get_main config in
182
  let ide  = match Whyconf.get_section config "ide" with
183
    | None -> default_ide
184 185
    | Some s -> load_ide s
  in
186 187
  set_labels_flag ide.ide_show_labels;
  set_locs_flag ide.ide_show_locs;
MARCHE Claude's avatar
MARCHE Claude committed
188 189 190
  { window_height = ide.ide_window_height;
    window_width  = ide.ide_window_width;
    tree_width    = ide.ide_tree_width;
191
    current_tab   = ide.ide_current_tab;
192
    font_size     = ide.ide_font_size;
MARCHE Claude's avatar
MARCHE Claude committed
193
    verbose       = ide.ide_verbose;
194 195 196
    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
197
    show_time_limit = ide.ide_show_time_limit;
MARCHE Claude's avatar
MARCHE Claude committed
198
    max_boxes = ide.ide_max_boxes;
199
    saving_policy = ide.ide_saving_policy ;
Andrei Paskevich's avatar
minor  
Andrei Paskevich committed
200
    premise_color = ide.ide_premise_color;
201
    neg_premise_color = ide.ide_neg_premise_color;
Andrei Paskevich's avatar
minor  
Andrei Paskevich committed
202
    goal_color = ide.ide_goal_color;
203
    error_color = ide.ide_error_color;
MARCHE Claude's avatar
MARCHE Claude committed
204
    iconset = ide.ide_iconset;
205
    default_prover = ide.ide_default_prover;
MARCHE Claude's avatar
MARCHE Claude committed
206 207
    default_editor = ide.ide_default_editor;
    config         = config;
208
    original_config = original_config;
209
    env            = env;
210
    hidden_provers = ide.ide_hidden_provers;
211 212 213
    session_time_limit = Whyconf.timelimit main;
    session_mem_limit = Whyconf.memlimit main;
    session_nb_processes = Whyconf.running_provers_max main;
214
    session_cntexample = Whyconf.cntexample main;
215
}
MARCHE Claude's avatar
MARCHE Claude committed
216

217
let save_config t =
MARCHE Claude's avatar
MARCHE Claude committed
218
  Debug.dprintf debug "[GUI config] saving IDE config file@.";
219
  (* taking original config, without the extra_config *)
220
  let config = t.original_config in
221 222 223 224 225 226
  (* 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
227 228 229
  let new_main = Whyconf.get_main t.config in
  let cntexample = Whyconf.cntexample new_main in
  let config = set_main config (set_cntexample (get_main config) cntexample) in
230 231 232 233
  (* 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 *)
234
  let config = set_policies config (get_policies t.config) in
235 236 237 238
  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
239
  let ide = set_int ide "current_tab" t.current_tab in
240
  let ide = set_int ide "font_size" t.font_size in
241
  let ide = set_int ide "verbose" t.verbose in
242 243 244
  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
245
  let ide = set_bool ide "print_time_limit" t.show_time_limit in
MARCHE Claude's avatar
MARCHE Claude committed
246
  let ide = set_int ide "max_boxes" t.max_boxes in
247
  let ide = set_int ide "saving_policy" t.saving_policy in
Andrei Paskevich's avatar
minor  
Andrei Paskevich committed
248
  let ide = set_string ide "premise_color" t.premise_color in
249
  let ide = set_string ide "neg_premise_color" t.neg_premise_color in
Andrei Paskevich's avatar
minor  
Andrei Paskevich committed
250
  let ide = set_string ide "goal_color" t.goal_color in
251
  let ide = set_string ide "error_color" t.error_color in
MARCHE Claude's avatar
MARCHE Claude committed
252
  let ide = set_string ide "iconset" t.iconset in
253
  let ide = set_string ide "default_prover" t.default_prover in
254
  let ide = set_string ide "default_editor" t.default_editor in
255
  let ide = set_stringl ide "hidden_prover" t.hidden_provers in
256
  let config = Whyconf.set_section config "ide" ide in
257
  Whyconf.save_config config
MARCHE Claude's avatar
MARCHE Claude committed
258

259
let config,load_config =
260 261 262 263 264
  let config = ref None in
  (fun () ->
    match !config with
      | None -> invalid_arg "configuration not yet loaded"
      | Some conf -> conf),
265 266
  (fun conf base_conf env ->
    let c = load_config conf base_conf env in
267
    config := Some c)
268

269
let save_config () = save_config (config ())
270

271
let get_main () = (get_main (config ()).config)
272

273 274 275 276 277
let incr_font_size n =
  let c = config () in
  let s = max (c.font_size + n) 4 in
  c.font_size <- s;
  s
278

MARCHE Claude's avatar
MARCHE Claude committed
279 280
(*

MARCHE Claude's avatar
MARCHE Claude committed
281
  images, icons
MARCHE Claude's avatar
MARCHE Claude committed
282 283 284

*)

François Bobot's avatar
François Bobot committed
285
let image_default = ref (GdkPixbuf.create ~width:1 ~height:1 ())
286
(* dumb pixbuf *)
MARCHE Claude's avatar
MARCHE Claude committed
287
let image_undone = ref !image_default
MARCHE Claude's avatar
MARCHE Claude committed
288 289 290 291 292 293
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
294
let image_outofmemory = ref !image_default
295
let image_steplimitexceeded = ref !image_default
MARCHE Claude's avatar
MARCHE Claude committed
296
let image_failure = ref !image_default
297 298 299 300
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
301
let image_outofmemory_obs = ref !image_default
302
let image_steplimitexceeded_obs = ref !image_default
303
let image_failure_obs = ref !image_default
MARCHE Claude's avatar
MARCHE Claude committed
304 305 306
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
307 308
let image_theory = ref !image_default
let image_goal = ref !image_default
MARCHE Claude's avatar
MARCHE Claude committed
309 310
let image_prover = ref !image_default
let image_transf = ref !image_default
François Bobot's avatar
François Bobot committed
311
let image_metas = ref !image_default
MARCHE Claude's avatar
MARCHE Claude committed
312
let image_editor = ref !image_default
313
let image_replay = ref !image_default
314
let image_cancel = ref !image_default
MARCHE Claude's avatar
MARCHE Claude committed
315
let image_reload = ref !image_default
MARCHE Claude's avatar
merge  
MARCHE Claude committed
316
let image_remove = ref !image_default
317
let image_cleaning = ref !image_default
MARCHE Claude's avatar
MARCHE Claude committed
318

MARCHE Claude's avatar
MARCHE Claude committed
319 320
let why_icon = ref !image_default

MARCHE Claude's avatar
MARCHE Claude committed
321 322
let image ?size f =
  let main = get_main () in
323
  let n =
MARCHE Claude's avatar
MARCHE Claude committed
324 325 326 327 328 329 330 331
    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
332 333 334 335 336 337 338 339 340 341

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 ""
342
let iconname_steplimitexceeded = ref ""
343 344 345 346 347 348
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 ""
349
let iconname_steplimitexceeded_obs = ref ""
350 351 352 353
let iconname_failure_obs = ref ""
let iconname_yes = ref ""
let iconname_no = ref ""
let iconname_file = ref ""
MARCHE Claude's avatar
MARCHE Claude committed
354 355
let iconname_theory = ref ""
let iconname_goal = ref ""
356 357
let iconname_prover = ref ""
let iconname_transf = ref ""
François Bobot's avatar
François Bobot committed
358
let iconname_metas  = ref ""
359 360 361 362 363 364 365
let iconname_editor = ref ""
let iconname_replay = ref ""
let iconname_cancel = ref ""
let iconname_reload = ref ""
let iconname_remove = ref ""
let iconname_cleaning = ref ""

366
let iconsets () : (string * Why3.Rc.family) =
367
  let main = get_main () in
MARCHE Claude's avatar
MARCHE Claude committed
368
  let dir = Filename.concat (datadir main) "images" in
369 370 371 372 373 374 375 376 377 378
  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)
379 380 381 382

let load_icon_names () =
  let ide = config () in
  let iconset = ide.iconset in
MARCHE Claude's avatar
MARCHE Claude committed
383 384 385 386 387 388 389 390 391 392
  let _,iconsets = iconsets () in
  let d =
    try
      List.assoc iconset iconsets
    with Not_found ->
      try
        List.assoc "fatcow" iconsets
      with Not_found ->
        failwith "No icon set found"
  in
MARCHE Claude's avatar
MARCHE Claude committed
393 394 395 396 397 398 399 400 401 402 403 404
  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";
405
  iconname_steplimitexceeded := get_icon_name "steplimitexceeded";
MARCHE Claude's avatar
MARCHE Claude committed
406 407 408 409 410 411
  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";
412
  iconname_steplimitexceeded_obs := get_icon_name "steplimitexceeded_obs";
MARCHE Claude's avatar
MARCHE Claude committed
413 414 415 416 417 418 419 420
  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
421
  iconname_metas  := get_icon_name "metas";
MARCHE Claude's avatar
MARCHE Claude committed
422 423 424 425 426 427
  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";
428 429
  ()

MARCHE Claude's avatar
MARCHE Claude committed
430
let resize_images size =
431 432 433 434 435 436 437 438 439
  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;
440
  image_steplimitexceeded := image ~size !iconname_steplimitexceeded;
441 442 443 444 445 446
  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;
447
  image_steplimitexceeded_obs := image ~size !iconname_steplimitexceeded_obs;
448 449 450 451
  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
452 453
  image_theory := image ~size !iconname_theory;
  image_goal := image ~size !iconname_goal;
454 455
  image_prover := image ~size !iconname_prover;
  image_transf := image ~size !iconname_transf;
François Bobot's avatar
François Bobot committed
456
  image_metas := image ~size !iconname_metas;
457 458 459 460 461 462
  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
463 464
  ()

465
let init () =
MARCHE Claude's avatar
MARCHE Claude committed
466
  Debug.dprintf debug "[GUI config] reading icons...@?";
467
  load_icon_names ();
MARCHE Claude's avatar
MARCHE Claude committed
468
  why_icon := image "logo-why";
MARCHE Claude's avatar
MARCHE Claude committed
469
  resize_images 20;
470
  Debug.dprintf debug " done.@."
MARCHE Claude's avatar
MARCHE Claude committed
471 472

let show_legend_window () =
473 474 475 476 477
  let dialog =
    GWindow.dialog
      ~title:"Why3: legend of icons" ~icon:!why_icon
      ()
  in
MARCHE Claude's avatar
MARCHE Claude committed
478
  let vbox = dialog#vbox in
479 480
  let text = GText.view ~packing:vbox#add
    ~editable:false ~cursor_visible:false () in
MARCHE Claude's avatar
MARCHE Claude committed
481
  let b = text#buffer in
482 483
  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
484
  let i s = b#insert ~iter:b#end_iter s in
485
  let it s = b#insert ~iter:b#end_iter ~tags:[tt] s in
MARCHE Claude's avatar
MARCHE Claude committed
486
  let ib i = b#insert_pixbuf ~iter:b#end_iter ~pixbuf:!i in
487
  it "Tree view\n";
MARCHE Claude's avatar
MARCHE Claude committed
488
  ib image_file;
MARCHE Claude's avatar
MARCHE Claude committed
489 490 491 492
  i "   File, containing a set of theories\n";
  ib image_theory;
  i "   Theory, containing a set of goals\n";
  ib image_goal;
493
  i "   Goal\n";
MARCHE Claude's avatar
MARCHE Claude committed
494
  ib image_prover;
495
  i "   External prover\n";
MARCHE Claude's avatar
MARCHE Claude committed
496
  ib image_transf;
MARCHE Claude's avatar
MARCHE Claude committed
497
  i "   Transformation or strategy\n";
498
  it "Status column\n";
499 500
  ib image_undone;
  i "   External proof attempt not done\n";
MARCHE Claude's avatar
MARCHE Claude committed
501
  ib image_scheduled;
502
  i "   Scheduled external proof attempt\n";
MARCHE Claude's avatar
MARCHE Claude committed
503
  ib image_running;
504
  i "   Running external proof attempt\n";
MARCHE Claude's avatar
MARCHE Claude committed
505
  ib image_valid;
506 507 508
  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
509
  ib image_timeout;
510
  i "   External prover reached the time limit\n";
511 512
  ib image_outofmemory;
  i "   External prover ran out of memory\n";
513 514
  ib image_steplimitexceeded;
  i "   External prover exceeded the step limit\n";
MARCHE Claude's avatar
MARCHE Claude committed
515
  ib image_unknown;
516
  i "   External prover answer not conclusive\n";
MARCHE Claude's avatar
MARCHE Claude committed
517
  ib image_failure;
518
  i "   External prover call failed\n";
519 520 521 522 523 524 525 526
  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
527
  dialog#add_button "Close" `CLOSE ;
528 529
  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
530 531 532 533 534
  let ( _ : GWindow.Buttons.about) = dialog#run () in
  dialog#destroy ()


let show_about_window () =
MARCHE Claude's avatar
MARCHE Claude committed
535 536
  let about_dialog =
    GWindow.about_dialog
Andrei Paskevich's avatar
Andrei Paskevich committed
537
      ~name:"The Why3 Verification Platform "
MARCHE Claude's avatar
MARCHE Claude committed
538 539 540
      ~authors:["François Bobot";
                "Jean-Christophe Filliâtre";
                "Claude Marché";
Andrei Paskevich's avatar
Andrei Paskevich committed
541 542 543 544 545
                "Guillaume Melquiond";
                "Andrei Paskevich";
                "";
                "with contributions of";
                "";
546
                "Stefan Berghofer";
Andrei Paskevich's avatar
Andrei Paskevich committed
547
                "Sylvie Boldo";
548
                "Martin Clochard";
Andrei Paskevich's avatar
Andrei Paskevich committed
549
                "Simon Cruanes";
550
                "Clément Fumex";
Andrei Paskevich's avatar
Andrei Paskevich committed
551
                "Leon Gondelman";
552
                "David Hauzar";
553
                "Daisuke Ishii";
Andrei Paskevich's avatar
Andrei Paskevich committed
554
                "Johannes Kanig";
MARCHE Claude's avatar
MARCHE Claude committed
555
                "Mikhail Mandrykin";
Andrei Paskevich's avatar
Andrei Paskevich committed
556 557 558 559
                "David Mentré";
                "Benjamin Monate";
                "Thi-Minh-Tuyen Nguyen";
                "Simão Melo de Sousa";
560 561 562
                "Asma Tafat";
                "Piotr Trojanek";
                "Makarius Wenzel";
MARCHE Claude's avatar
MARCHE Claude committed
563
               ]
Andrei Paskevich's avatar
Andrei Paskevich committed
564
      ~copyright:"Copyright 2010-2016 Inria, CNRS, Paris-Sud University"
MARCHE Claude's avatar
MARCHE Claude committed
565
      ~license:("See file " ^ Filename.concat Config.datadir "LICENSE")
Andrei Paskevich's avatar
Andrei Paskevich committed
566 567
      ~website:"http://why3.lri.fr"
      ~website_label:"http://why3.lri.fr"
MARCHE Claude's avatar
MARCHE Claude committed
568
      ~version:Config.version
MARCHE Claude's avatar
MARCHE Claude committed
569
      ()
MARCHE Claude's avatar
MARCHE Claude committed
570
  in
MARCHE Claude's avatar
MARCHE Claude committed
571 572
  let ( _ : GWindow.Buttons.about) = about_dialog#run () in
  about_dialog#destroy ()
MARCHE Claude's avatar
MARCHE Claude committed
573

574

575

MARCHE Claude's avatar
MARCHE Claude committed
576 577 578

(**** Preferences Window ***)

579
let general_settings (c : t) (notebook:GPack.notebook) =
MARCHE Claude's avatar
MARCHE Claude committed
580 581
  let label = GMisc.label ~text:"General" () in
  let page =
MARCHE Claude's avatar
MARCHE Claude committed
582
    GPack.vbox ~homogeneous:false ~packing:
MARCHE Claude's avatar
MARCHE Claude committed
583
      (fun w -> ignore(notebook#append_page ~tab_label:label#coerce w)) ()
MARCHE Claude's avatar
MARCHE Claude committed
584
  in
585
  (* debug mode ? *)
MARCHE Claude's avatar
MARCHE Claude committed
586
(*
MARCHE Claude's avatar
MARCHE Claude committed
587
  let debugmode =
MARCHE Claude's avatar
MARCHE Claude committed
588
    GButton.check_button ~label:"debug" ~packing:page1#add ()
MARCHE Claude's avatar
MARCHE Claude committed
589 590
      ~active:(c.verbose > 0)
  in
MARCHE Claude's avatar
MARCHE Claude committed
591
  let (_ : GtkSignal.id) =
MARCHE Claude's avatar
MARCHE Claude committed
592 593
    debugmode#connect#toggled ~callback:
      (fun () -> c.verbose <- 1 - c.verbose)
MARCHE Claude's avatar
MARCHE Claude committed
594
  in
MARCHE Claude's avatar
MARCHE Claude committed
595
*)
596
  let page_pack = page#pack ?from:None ?expand:None ?fill:None ?padding:None in
597
  let external_processes_options_frame =
598
    GBin.frame ~label:"External provers options" ~packing:page_pack ()
599 600 601 602
  in
  let vb = GPack.vbox ~homogeneous:false
    ~packing:external_processes_options_frame#add ()
  in
603
  (* time limit *)
604 605 606
  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
607
  let _ = GMisc.label ~text:"Time limit (in sec.): " ~width ~xalign
608
    ~packing:hb_pack () in
609
  let timelimit_spin = GEdit.spin_button ~digits:0 ~packing:hb#add () in
MARCHE Claude's avatar
MARCHE Claude committed
610
  timelimit_spin#adjustment#set_bounds ~lower:0. ~upper:86_400. ~step_incr:5. ();
611
  timelimit_spin#adjustment#set_value (float_of_int c.session_time_limit);
MARCHE Claude's avatar
MARCHE Claude committed
612
  let (_ : GtkSignal.id) =
613
    timelimit_spin#connect#value_changed ~callback:
614
      (fun () -> c.session_time_limit <- timelimit_spin#value_as_int)
615
  in
616
  (* mem limit *)
617 618
  let hb = GPack.hbox ~homogeneous:false ~packing:vb#add () in
  let hb_pack = hb#pack ~expand:false ?from:None ?fill:None ?padding:None in
619
  let _ = GMisc.label ~text:"Memory limit (in Mb): " ~width ~xalign
620
    ~packing:hb_pack () in
621
  let memlimit_spin = GEdit.spin_button ~digits:0 ~packing:hb#add () in
MARCHE Claude's avatar
MARCHE Claude committed
622
  memlimit_spin#adjustment#set_bounds ~lower:0. ~upper:16_000. ~step_incr:500. ();
623
  memlimit_spin#adjustment#set_value (float_of_int c.session_mem_limit);
624 625
  let (_ : GtkSignal.id) =
    memlimit_spin#connect#value_changed ~callback:
626 627 628
      (fun () -> c.session_mem_limit <- memlimit_spin#value_as_int)
  in
  (* nb of processes *)
629 630
  let hb = GPack.hbox ~homogeneous:false ~packing:vb#add () in
  let hb_pack = hb#pack ~expand:false ?from:None ?fill:None ?padding:None in
631
  let _ = GMisc.label ~text:"Nb of processes: " ~width ~xalign
632
    ~packing:hb_pack () in
MARCHE Claude's avatar
MARCHE Claude committed
633
  let nb_processes_spin = GEdit.spin_button ~digits:0 ~packing:hb#add () in
634
  nb_processes_spin#adjustment#set_bounds
MARCHE Claude's avatar
MARCHE Claude committed
635
    ~lower:1. ~upper:64. ~step_incr:1. ();
636
  nb_processes_spin#adjustment#set_value
637
    (float_of_int c.session_nb_processes);
MARCHE Claude's avatar
MARCHE Claude committed
638
  let (_ : GtkSignal.id) =
MARCHE Claude's avatar
MARCHE Claude committed
639
    nb_processes_spin#connect#value_changed ~callback:
640 641
      (fun () -> c.session_nb_processes <- nb_processes_spin#value_as_int)
  in
642 643 644 645 646 647 648 649 650
  (* counter-example *)
  let cntexample_check = GButton.check_button ~label:"get counter-example"
    ~packing:vb#add ()
    ~active:c.session_cntexample
  in
  let (_: GtkSignal.id) =
    cntexample_check#connect#toggled ~callback:
      (fun () -> c.session_cntexample <- not c.session_cntexample)
  in
651 652 653 654 655 656 657 658 659 660 661 662 663 664 665 666 667 668 669 670 671 672 673 674 675 676 677 678 679 680 681 682 683 684 685 686 687 688 689 690 691 692 693 694 695 696 697 698 699 700 701 702 703 704 705
  (* 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
706
  let display_options_frame =
707
    GBin.frame ~label:"Display options" ~packing:page_pack ()
708
  in
709 710
  let vb = GPack.vbox ~homogeneous:false
    ~packing:display_options_frame#add ()
711
  in
MARCHE Claude's avatar
MARCHE Claude committed
712
  (* max boxes *)
713 714
  let width = 300 and xalign = 0.0 in
  let hb = GPack.hbox ~homogeneous:false ~packing:vb#add () in
715
  let hb_pack = hb#pack ~expand:false ?fill:None ?from:None ?padding:None in
716
  let _ = GMisc.label ~text:"Use ellipsis for terms deeper than: " ~width ~xalign ~packing:hb_pack () in
MARCHE Claude's avatar
MARCHE Claude committed
717 718 719 720 721 722 723
  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
724 725 726 727 728
  (* options for task display *)
  let display_options_box =
    GPack.button_box `VERTICAL ~border_width:5 ~spacing:5
      ~packing:vb#add ()
  in
729 730 731 732 733 734 735 736 737
  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
738
  let showlabels =
739 740
    GButton.check_button
      ~label:"show labels in formulas"
741
      ~packing:display_options_box#add ()
742
      ~active:c.show_labels
743 744 745
  in
  let (_ : GtkSignal.id) =
    showlabels#connect#toggled ~callback:
746 747
      (fun () ->
         c.show_labels <- not c.show_labels;
748 749
         set_labels_flag c.show_labels)
  in
750
  let showlocs =
751 752
    GButton.check_button
      ~label:"show source locations in formulas"
753
      ~packing:display_options_box#add ()
754
      ~active:c.show_locs
755 756 757
  in
  let (_ : GtkSignal.id) =
    showlocs#connect#toggled ~callback:
758 759
      (fun () ->
         c.show_locs <- not c.show_locs;
760 761
         set_locs_flag c.show_locs)
  in
MARCHE Claude's avatar
MARCHE Claude committed
762 763
  let showtimelimit =
    GButton.check_button
Claude Marche's avatar
Claude Marche committed
764
      ~label:"show time and memory limits for each proof"
MARCHE Claude's avatar
MARCHE Claude committed
765 766 767 768 769 770 771 772
      ~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
773 774 775
  (* icon sets *)
  let icon_sets_frame =
    GBin.frame ~label:"Change icon family (needs save & restart)"
776
      ~packing:page_pack ()
777
  in
778
  let icon_sets_box =
779 780
    GPack.button_box
      `VERTICAL ~border_width:5 ~spacing:5
781 782 783 784 785
      ~packing:icon_sets_frame#add ()
  in
  let icon_sets_box_pack =
    icon_sets_box#pack ?from:None ?expand:None ?fill:None ?padding:None
  in
MARCHE Claude's avatar
MARCHE Claude committed
786
  let dir,iconsets = iconsets () in
787 788
  let set_icon_set s () = c.iconset <- s in
  let (_,choices) = List.fold_left
MARCHE Claude's avatar
MARCHE Claude committed
789 790 791 792 793 794 795 796 797 798 799 800 801 802 803 804 805 806 807 808 809 810 811 812 813 814 815 816 817 818 819 820 821 822 823 824 825 826
    (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
827 828 829 830 831 832 833
  in