gconfig.ml 42.5 KB
Newer Older
Andrei Paskevich's avatar
Andrei Paskevich committed
1 2 3
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
Guillaume Melquiond's avatar
Guillaume Melquiond committed
4
(*  Copyright 2010-2018   --   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 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;
MARCHE Claude's avatar
MARCHE Claude committed
45
      mutable max_boxes : int;
46
      mutable allow_source_editing : bool;
47
      mutable saving_policy : int;
48
      (** 0 = always, 1 = never, 2 = ask *)
Andrei Paskevich's avatar
minor  
Andrei Paskevich committed
49
      mutable premise_color : string;
50
      mutable neg_premise_color : string;
Andrei Paskevich's avatar
minor  
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;
MARCHE Claude's avatar
MARCHE Claude committed
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 62 63
      mutable session_time_limit : int;
      mutable session_mem_limit : int;
      mutable session_nb_processes : int;
MARCHE Claude's avatar
MARCHE Claude committed
64 65
    }

MARCHE Claude's avatar
MARCHE Claude committed
66

67 68 69 70
type ide = {
  ide_window_width : int;
  ide_window_height : int;
  ide_tree_width : int;
71
  ide_task_height : int;
72
  ide_font_size : int;
73
  ide_current_tab : int;
74
  ide_verbose : int;
75
  ide_show_full_context : bool;
76
  ide_show_attributes : bool;
Mário Pereira's avatar
Mário Pereira committed
77
  ide_show_coercions : bool;
78
  ide_show_locs : bool;
MARCHE Claude's avatar
MARCHE Claude committed
79
  ide_show_time_limit : bool;
MARCHE Claude's avatar
MARCHE Claude committed
80
  ide_max_boxes : int;
81
  ide_allow_source_editing : bool;
82
  ide_saving_policy : int;
Andrei Paskevich's avatar
minor  
Andrei Paskevich committed
83
  ide_premise_color : string;
84
  ide_neg_premise_color : string;
Andrei Paskevich's avatar
minor  
Andrei Paskevich committed
85
  ide_goal_color : string;
86
  ide_error_color : string;
87
  ide_error_color_bg : string;
88
  ide_error_line_color : string;
MARCHE Claude's avatar
MARCHE Claude committed
89
  ide_iconset : string;
90
  (* ide_replace_prover : conf_replace_prover; *)
91
}
MARCHE Claude's avatar
MARCHE Claude committed
92

93 94 95 96
let default_ide =
  { ide_window_width = 1024;
    ide_window_height = 768;
    ide_tree_width = 512;
97
    ide_task_height = 400;
98
    ide_font_size = 10;
99
    ide_current_tab = 0;
100
    ide_verbose = 0;
101
    ide_show_full_context = false;
102
    ide_show_attributes = false;
Mário Pereira's avatar
Mário Pereira committed
103
    ide_show_coercions = true;
104
    ide_show_locs = false;
MARCHE Claude's avatar
MARCHE Claude committed
105
    ide_show_time_limit = false;
MARCHE Claude's avatar
MARCHE Claude committed
106
    ide_max_boxes = 16;
107
    ide_allow_source_editing = true;
108
    ide_saving_policy = 2;
Andrei Paskevich's avatar
minor  
Andrei Paskevich committed
109
    ide_premise_color = "chartreuse";
110
    ide_neg_premise_color = "pink";
Andrei Paskevich's avatar
minor  
Andrei Paskevich committed
111
    ide_goal_color = "gold";
112
    ide_error_color_bg = "yellow";
113 114
    ide_error_color = "red";
    ide_error_line_color = "yellow";
MARCHE Claude's avatar
MARCHE Claude committed
115
    ide_iconset = "fatcow";
116 117 118 119 120 121 122 123 124
  }

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";
125 126
    ide_task_height =
      get_int section ~default:default_ide.ide_task_height "task_height";
127 128
    ide_current_tab =
      get_int section ~default:default_ide.ide_current_tab "current_tab";
129 130
    ide_font_size =
      get_int section ~default:default_ide.ide_font_size "font_size";
131 132
    ide_verbose =
      get_int section ~default:default_ide.ide_verbose "verbose";
133 134 135
    ide_show_full_context =
      get_bool section ~default:default_ide.ide_show_full_context
        "show_full_context";
136 137
    ide_show_attributes =
      get_bool section ~default:default_ide.ide_show_attributes "print_attributes";
Mário Pereira's avatar
Mário Pereira committed
138
    ide_show_coercions =
139
      get_bool section ~default:default_ide.ide_show_attributes "print_coercions";
140 141
    ide_show_locs =
      get_bool section ~default:default_ide.ide_show_locs "print_locs";
MARCHE Claude's avatar
MARCHE Claude committed
142
    ide_show_time_limit =
143 144
      get_bool section ~default:default_ide.ide_show_time_limit
        "print_time_limit";
MARCHE Claude's avatar
MARCHE Claude committed
145 146 147
    ide_max_boxes =
      get_int section ~default:default_ide.ide_max_boxes
        "max_boxes";
148 149
    ide_allow_source_editing =
      get_bool section ~default:default_ide.ide_allow_source_editing "allow_source_editing";
150 151
    ide_saving_policy =
      get_int section ~default:default_ide.ide_saving_policy "saving_policy";
Andrei Paskevich's avatar
minor  
Andrei Paskevich committed
152 153 154
    ide_premise_color =
      get_string section ~default:default_ide.ide_premise_color
        "premise_color";
155 156 157
    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
158 159 160
    ide_goal_color =
      get_string section ~default:default_ide.ide_goal_color
        "goal_color";
161 162 163
    ide_error_color =
      get_string section ~default:default_ide.ide_error_color
        "error_color";
164 165 166
    ide_error_color_bg =
      get_string section ~default:default_ide.ide_error_color_bg
        "error_color_bg";
167 168 169
    ide_error_line_color =
      get_string section ~default:default_ide.ide_error_line_color
        "error_line_color";
170
    ide_iconset =
MARCHE Claude's avatar
MARCHE Claude committed
171 172
      get_string section ~default:default_ide.ide_iconset
        "iconset";
173
  }
MARCHE Claude's avatar
MARCHE Claude committed
174

175

176 177
let set_attr_flag =
  let fl = Debug.lookup_flag "print_attributes" in
178 179 180
  fun b ->
    (if b then Debug.set_flag else Debug.unset_flag) fl

Mário Pereira's avatar
Mário Pereira committed
181 182 183 184 185
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

186 187 188 189 190
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
191
let load_config config original_config =
Andrei Paskevich's avatar
Andrei Paskevich committed
192
  let main = get_main config in
193
  let ide  = match Whyconf.get_section config "ide" with
194
    | None -> default_ide
195 196
    | Some s -> load_ide s
  in
197
  set_attr_flag ide.ide_show_attributes;
Mário Pereira's avatar
Mário Pereira committed
198
  set_coercions_flag ide.ide_show_coercions;
199
  set_locs_flag ide.ide_show_locs;
MARCHE Claude's avatar
MARCHE Claude committed
200 201 202
  { window_height = ide.ide_window_height;
    window_width  = ide.ide_window_width;
    tree_width    = ide.ide_tree_width;
203
    task_height   = ide.ide_task_height;
204
    current_tab   = ide.ide_current_tab;
205
    font_size     = ide.ide_font_size;
MARCHE Claude's avatar
MARCHE Claude committed
206
    verbose       = ide.ide_verbose;
207
    show_full_context= ide.ide_show_full_context ;
208
    show_attributes   = ide.ide_show_attributes ;
Mário Pereira's avatar
Mário Pereira committed
209
    show_coercions = ide.ide_show_coercions ;
210
    show_locs     = ide.ide_show_locs ;
MARCHE Claude's avatar
MARCHE Claude committed
211
    show_time_limit = ide.ide_show_time_limit;
MARCHE Claude's avatar
MARCHE Claude committed
212
    max_boxes = ide.ide_max_boxes;
213
    allow_source_editing = ide.ide_allow_source_editing ;
214
    saving_policy = ide.ide_saving_policy ;
Andrei Paskevich's avatar
minor  
Andrei Paskevich committed
215
    premise_color = ide.ide_premise_color;
216
    neg_premise_color = ide.ide_neg_premise_color;
Andrei Paskevich's avatar
minor  
Andrei Paskevich committed
217
    goal_color = ide.ide_goal_color;
218
    error_color = ide.ide_error_color;
219
    error_color_bg = ide.ide_error_color_bg;
220
    error_line_color = ide.ide_error_line_color;
MARCHE Claude's avatar
MARCHE Claude committed
221
    iconset = ide.ide_iconset;
MARCHE Claude's avatar
MARCHE Claude committed
222
    config         = config;
223
    original_config = original_config;
224 225 226 227
    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
228

229
let save_config t =
230
  Debug.dprintf debug "[config] saving IDE config file@.";
231
  (* taking original config, without the extra_config *)
232
  let config = t.original_config in
233 234 235 236 237 238 239 240 241 242
  (* 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 *)
243
  let config = set_policies config (get_policies t.config) in
244 245 246 247
  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
248
  let ide = set_int ide "task_height" t.task_height in
249
  let ide = set_int ide "current_tab" t.current_tab in
250
  let ide = set_int ide "font_size" t.font_size in
251
  let ide = set_int ide "verbose" t.verbose in
252
  let ide = set_bool ide "show_full_context" t.show_full_context in
253
  let ide = set_bool ide "print_attributes" t.show_attributes in
Mário Pereira's avatar
Mário Pereira committed
254
  let ide = set_bool ide "print_coercions" t.show_coercions in
255
  let ide = set_bool ide "print_locs" t.show_locs in
MARCHE Claude's avatar
MARCHE Claude committed
256
  let ide = set_bool ide "print_time_limit" t.show_time_limit in
MARCHE Claude's avatar
MARCHE Claude committed
257
  let ide = set_int ide "max_boxes" t.max_boxes in
258
  let ide = set_bool ide "allow_source_editing" t.allow_source_editing in
259
  let ide = set_int ide "saving_policy" t.saving_policy in
Andrei Paskevich's avatar
minor  
Andrei Paskevich committed
260
  let ide = set_string ide "premise_color" t.premise_color in
261
  let ide = set_string ide "neg_premise_color" t.neg_premise_color in
Andrei Paskevich's avatar
minor  
Andrei Paskevich committed
262
  let ide = set_string ide "goal_color" t.goal_color in
263
  let ide = set_string ide "error_color" t.error_color in
264
  let ide = set_string ide "error_color_bg" t.error_color_bg in
265
  let ide = set_string ide "error_line_color" t.error_line_color in
MARCHE Claude's avatar
MARCHE Claude committed
266
  let ide = set_string ide "iconset" t.iconset in
267
  let config = Whyconf.set_section config "ide" ide in
268
  Whyconf.save_config config
MARCHE Claude's avatar
MARCHE Claude committed
269

270
let config,load_config =
271 272 273 274 275
  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
276 277
  (fun conf base_conf ->
    let c = load_config conf base_conf in
278
    config := Some c)
279

280
let save_config () = save_config (config ())
281

282
let get_main () = (get_main (config ()).config)
283

MARCHE Claude's avatar
MARCHE Claude committed
284 285 286 287 288 289 290 291 292 293 294 295 296 297 298 299 300 301 302 303 304 305 306 307 308 309 310 311 312 313 314 315
(*


  font size


 *)


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

let modifiable_sans_font_views = ref []
let modifiable_mono_font_views = ref []

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
  let sf = Pango.Font.from_string sff in
  let mf = Pango.Font.from_string mff in
  List.iter (fun v -> v#modify_font sf) !modifiable_sans_font_views;
  List.iter (fun v -> v#modify_font mf) !modifiable_mono_font_views

316 317 318 319 320
let incr_font_size n =
  let c = config () in
  let s = max (c.font_size + n) 4 in
  c.font_size <- s;
  s
321

Clément Fumex's avatar
Clément Fumex committed
322
let enlarge_fonts () = change_font (incr_font_size 1)
MARCHE Claude's avatar
MARCHE Claude committed
323

Clément Fumex's avatar
Clément Fumex committed
324
let reduce_fonts () = change_font (incr_font_size (-1))
MARCHE Claude's avatar
MARCHE Claude committed
325

Clément Fumex's avatar
Clément Fumex committed
326
let set_fonts () = change_font (incr_font_size 0)
MARCHE Claude's avatar
MARCHE Claude committed
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
let image_default = ref (GdkPixbuf.create ~width:1 ~height:1 ())
335
(* 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
344
let image_steplimitexceeded = ref !image_default
MARCHE Claude's avatar
MARCHE Claude committed
345
let image_failure = ref !image_default
346 347 348 349
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
350
let image_outofmemory_obs = ref !image_default
351
let image_steplimitexceeded_obs = ref !image_default
352
let image_failure_obs = ref !image_default
MARCHE Claude's avatar
MARCHE Claude committed
353 354 355
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
356 357
let image_theory = ref !image_default
let image_goal = ref !image_default
MARCHE Claude's avatar
MARCHE Claude committed
358 359
let image_prover = ref !image_default
let image_transf = ref !image_default
François Bobot's avatar
François Bobot committed
360
let image_metas = ref !image_default
MARCHE Claude's avatar
MARCHE Claude committed
361
let image_editor = ref !image_default
362
let image_replay = ref !image_default
363
let image_cancel = ref !image_default
MARCHE Claude's avatar
MARCHE Claude committed
364
let image_reload = ref !image_default
MARCHE Claude's avatar
merge  
MARCHE Claude committed
365
let image_remove = ref !image_default
366
let image_cleaning = ref !image_default
MARCHE Claude's avatar
MARCHE Claude committed
367

MARCHE Claude's avatar
MARCHE Claude committed
368 369
let why_icon = ref !image_default

MARCHE Claude's avatar
MARCHE Claude committed
370 371
let image ?size f =
  let main = get_main () in
372
  let n =
MARCHE Claude's avatar
MARCHE Claude committed
373 374 375
    Filename.concat (datadir main)
      (Filename.concat "images" (f^".png"))
  in
376
  try (
MARCHE Claude's avatar
MARCHE Claude committed
377 378 379 380 381
  match size with
    | None ->
        GdkPixbuf.from_file n
    | Some s ->
        GdkPixbuf.from_file_at_size ~width:s ~height:s n
382
  ) with _ -> !image_default
383 384 385 386 387 388 389 390 391 392

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 ""
393
let iconname_steplimitexceeded = ref ""
394 395 396 397 398 399
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 ""
400
let iconname_steplimitexceeded_obs = ref ""
401 402 403 404
let iconname_failure_obs = ref ""
let iconname_yes = ref ""
let iconname_no = ref ""
let iconname_file = ref ""
MARCHE Claude's avatar
MARCHE Claude committed
405 406
let iconname_theory = ref ""
let iconname_goal = ref ""
407 408
let iconname_prover = ref ""
let iconname_transf = ref ""
François Bobot's avatar
François Bobot committed
409
let iconname_metas  = ref ""
410 411 412 413 414 415 416
let iconname_editor = ref ""
let iconname_replay = ref ""
let iconname_cancel = ref ""
let iconname_reload = ref ""
let iconname_remove = ref ""
let iconname_cleaning = ref ""

417
let iconsets () : (string * Why3.Rc.family) =
418
  let main = get_main () in
MARCHE Claude's avatar
MARCHE Claude committed
419
  let dir = Filename.concat (datadir main) "images" in
420 421 422 423 424 425 426 427 428 429
  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)
430 431 432 433

let load_icon_names () =
  let ide = config () in
  let iconset = ide.iconset in
MARCHE Claude's avatar
MARCHE Claude committed
434
  let _,iconsets = iconsets () in
435
  let iconset,d =
MARCHE Claude's avatar
MARCHE Claude committed
436
    try
437
      iconset, List.assoc iconset iconsets
MARCHE Claude's avatar
MARCHE Claude committed
438 439
    with Not_found ->
      try
440
        "fatcow", List.assoc "fatcow" iconsets
MARCHE Claude's avatar
MARCHE Claude committed
441 442 443
      with Not_found ->
        failwith "No icon set found"
  in
MARCHE Claude's avatar
MARCHE Claude committed
444 445 446 447 448 449 450 451 452 453 454 455
  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";
456
  iconname_steplimitexceeded := get_icon_name "steplimitexceeded";
MARCHE Claude's avatar
MARCHE Claude committed
457 458 459 460 461 462
  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";
463
  iconname_steplimitexceeded_obs := get_icon_name "steplimitexceeded_obs";
MARCHE Claude's avatar
MARCHE Claude committed
464 465 466 467 468 469 470 471
  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
472
  iconname_metas  := get_icon_name "metas";
MARCHE Claude's avatar
MARCHE Claude committed
473 474 475 476 477 478
  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";
479 480
  ()

MARCHE Claude's avatar
MARCHE Claude committed
481
let resize_images size =
482 483 484 485 486 487 488 489 490
  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;
491
  image_steplimitexceeded := image ~size !iconname_steplimitexceeded;
492 493 494 495 496 497
  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;
498
  image_steplimitexceeded_obs := image ~size !iconname_steplimitexceeded_obs;
499 500 501 502
  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
503 504
  image_theory := image ~size !iconname_theory;
  image_goal := image ~size !iconname_goal;
505 506
  image_prover := image ~size !iconname_prover;
  image_transf := image ~size !iconname_transf;
François Bobot's avatar
François Bobot committed
507
  image_metas := image ~size !iconname_metas;
508 509 510 511 512 513
  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
514 515
  ()

516
let init () =
517
  Debug.dprintf debug "[config] reading icons...@?";
518
  load_icon_names ();
MARCHE Claude's avatar
MARCHE Claude committed
519
  why_icon := image "logo-why";
MARCHE Claude's avatar
MARCHE Claude committed
520
  resize_images 20;
521
  Debug.dprintf debug " done.@."
MARCHE Claude's avatar
MARCHE Claude committed
522 523

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


let show_about_window () =
MARCHE Claude's avatar
MARCHE Claude committed
592 593
  let about_dialog =
    GWindow.about_dialog
Guillaume Melquiond's avatar
Guillaume Melquiond committed
594
      ~name:"The Why3 Verification Platform"
MARCHE Claude's avatar
MARCHE Claude committed
595 596 597
      ~authors:["François Bobot";
                "Jean-Christophe Filliâtre";
                "Claude Marché";
Andrei Paskevich's avatar
Andrei Paskevich committed
598 599 600 601 602
                "Guillaume Melquiond";
                "Andrei Paskevich";
                "";
                "with contributions of";
                "";
603
                "Stefan Berghofer";
Andrei Paskevich's avatar
Andrei Paskevich committed
604
                "Sylvie Boldo";
605
                "Martin Clochard";
Andrei Paskevich's avatar
Andrei Paskevich committed
606
                "Simon Cruanes";
MARCHE Claude's avatar
MARCHE Claude committed
607
                "Sylvain Dailler";
Guillaume Melquiond's avatar
Guillaume Melquiond committed
608
                "Jacques-Pascal Deplaix";
609
                "Clément Fumex";
Andrei Paskevich's avatar
Andrei Paskevich committed
610
                "Leon Gondelman";
611
                "David Hauzar";
612
                "Daisuke Ishii";
Andrei Paskevich's avatar
Andrei Paskevich committed
613
                "Johannes Kanig";
MARCHE Claude's avatar
MARCHE Claude committed
614
                "Mikhail Mandrykin";
Andrei Paskevich's avatar
Andrei Paskevich committed
615 616
                "David Mentré";
                "Benjamin Monate";
Guillaume Melquiond's avatar
Guillaume Melquiond committed
617
                "Kim Nguyễn";
Andrei Paskevich's avatar
Andrei Paskevich committed
618 619
                "Thi-Minh-Tuyen Nguyen";
                "Simão Melo de Sousa";
620 621 622
                "Asma Tafat";
                "Piotr Trojanek";
                "Makarius Wenzel";
MARCHE Claude's avatar
MARCHE Claude committed
623
               ]
Guillaume Melquiond's avatar
Guillaume Melquiond committed
624
      ~copyright:"Copyright 2010-2018 Inria, CNRS, Paris-Sud University"
MARCHE Claude's avatar
MARCHE Claude committed
625
      ~license:("See file " ^ Filename.concat Config.datadir "LICENSE")
Guillaume Melquiond's avatar
Guillaume Melquiond committed
626 627
      ~website:"http://why3.lri.fr/"
      ~website_label:"http://why3.lri.fr/"
MARCHE Claude's avatar
MARCHE Claude committed
628
      ~version:Config.version
Guillaume Melquiond's avatar
Guillaume Melquiond committed
629 630
      ~icon:!why_icon
      ~logo:!why_icon
MARCHE Claude's avatar
MARCHE Claude committed
631
      ()
MARCHE Claude's avatar
MARCHE Claude committed
632
  in
MARCHE Claude's avatar
MARCHE Claude committed
633 634
  let ( _ : GWindow.Buttons.about) = about_dialog#run () in
  about_dialog#destroy ()
MARCHE Claude's avatar
MARCHE Claude committed
635

636

637

MARCHE Claude's avatar
MARCHE Claude committed
638 639 640

(**** Preferences Window ***)

641
let general_settings (c : t) (notebook:GPack.notebook) =
MARCHE Claude's avatar
MARCHE Claude committed
642 643
  let label = GMisc.label ~text:"General" () in
  let page =
MARCHE Claude's avatar
MARCHE Claude committed
644
    GPack.vbox ~homogeneous:false ~packing:
MARCHE Claude's avatar
MARCHE Claude committed
645
      (fun w -> ignore(notebook#append_page ~tab_label:label#coerce w)) ()
MARCHE Claude's avatar
MARCHE Claude committed
646
  in
647
  (* debug mode ? *)
MARCHE Claude's avatar
MARCHE Claude committed
648
(*
MARCHE Claude's avatar
MARCHE Claude committed
649
  let debugmode =
MARCHE Claude's avatar
MARCHE Claude committed
650
    GButton.check_button ~label:"debug" ~packing:page1#add ()
MARCHE Claude's avatar
MARCHE Claude committed
651 652
      ~active:(c.verbose > 0)
  in
MARCHE Claude's avatar
MARCHE Claude committed
653
  let (_ : GtkSignal.id) =
MARCHE Claude's avatar
MARCHE Claude committed
654 655
    debugmode#connect#toggled ~callback:
      (fun () -> c.verbose <- 1 - c.verbose)
MARCHE Claude's avatar
MARCHE Claude committed
656
  in
MARCHE Claude's avatar
MARCHE Claude committed
657
*)
658
  let page_pack = page#pack ?from:None ?expand:None ?fill:None ?padding:None in
659
  let external_processes_options_frame =
660
    GBin.frame ~label:"External provers options" ~packing:page_pack ()
661 662 663 664
  in
  let vb = GPack.vbox ~homogeneous:false
    ~packing:external_processes_options_frame#add ()
  in
665
  (* time limit *)
666 667 668
  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
669
  let _ = GMisc.label ~text:"Time limit (in sec.): " ~width ~xalign
670
    ~packing:hb_pack () in
671
  let timelimit_spin = GEdit.spin_button ~digits:0 ~packing:hb#add () in
MARCHE Claude's avatar
MARCHE Claude committed
672
  timelimit_spin#adjustment#set_bounds ~lower:0. ~upper:86_400. ~step_incr:5. ();
673
  timelimit_spin#adjustment#set_value (float_of_int c.session_time_limit);
MARCHE Claude's avatar
MARCHE Claude committed
674
  let (_ : GtkSignal.id) =
675
    timelimit_spin#connect#value_changed ~callback:
676
      (fun () -> c.session_time_limit <- timelimit_spin#value_as_int)
677
  in
678
  (* mem limit *)
679 680
  let hb = GPack.hbox ~homogeneous:false ~packing:vb#add () in
  let hb_pack = hb#pack ~expand:false ?from:None ?fill:None ?padding:None in
681
  let _ = GMisc.label ~text:"Memory limit (in Mb): " ~width ~xalign
682
    ~packing:hb_pack () in
683
  let memlimit_spin = GEdit.spin_button ~digits:0 ~packing:hb#add () in
MARCHE Claude's avatar
MARCHE Claude committed
684
  memlimit_spin#adjustment#set_bounds ~lower:0. ~upper:16_000. ~step_incr:500. ();
685
  memlimit_spin#adjustment#set_value (float_of_int c.session_mem_limit);
686 687
  let (_ : GtkSignal.id) =
    memlimit_spin#connect#value_changed ~callback:
688 689 690
      (fun () -> c.session_mem_limit <- memlimit_spin#value_as_int)
  in
  (* nb of processes *)
691 692
  let hb = GPack.hbox ~homogeneous:false ~packing:vb#add () in
  let hb_pack = hb#pack ~expand:false ?from:None ?fill:None ?padding:None in
693
  let _ = GMisc.label ~text:"Nb of processes: " ~width ~xalign
694
    ~packing:hb_pack () in
MARCHE Claude's avatar
MARCHE Claude committed
695
  let nb_processes_spin = GEdit.spin_button ~digits:0 ~packing:hb#add () in
696
  nb_processes_spin#adjustment#set_bounds
MARCHE Claude's avatar
MARCHE Claude committed
697
    ~lower:1. ~upper:64. ~step_incr:1. ();
698
  nb_processes_spin#adjustment#set_value
699
    (float_of_int c.session_nb_processes);
MARCHE Claude's avatar
MARCHE Claude committed
700
  let (_ : GtkSignal.id) =
MARCHE Claude's avatar
MARCHE Claude committed
701
    nb_processes_spin#connect#value_changed ~callback:
702 703
      (fun () -> c.session_nb_processes <- nb_processes_spin#value_as_int)
  in
704
  (* counter-example *)
705
(*
706 707 708 709 710 711 712 713
  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
714
*)
715 716 717 718 719 720 721 722 723
  (* 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
724 725 726 727 728 729 730 731 732 733 734 735 736 737 738 739 740 741 742 743 744 745 746 747 748 749 750 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
  (* 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
779
  let display_options_frame =
780
    GBin.frame ~label:"Display options" ~packing:page_pack ()
781
  in
782 783
  let vb = GPack.vbox ~homogeneous:false
    ~packing:display_options_frame#add ()
784
  in
MARCHE Claude's avatar
MARCHE Claude committed
785
  (* max boxes *)
786 787
  let width = 300 and xalign = 0.0 in
  let hb = GPack.hbox ~homogeneous:false ~packing:vb#add () in
788
  let hb_pack = hb#pack ~expand:false ?fill:None ?from:None ?padding:None in
789
  let _ = GMisc.label ~text:"Use ellipsis for terms deeper than: " ~width ~xalign ~packing:hb_pack () in
MARCHE Claude's avatar
MARCHE Claude committed
790 791 792 793 794 795 796
  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
797 798 799 800 801
  (* options for task display *)
  let display_options_box =
    GPack.button_box `VERTICAL ~border_width:5 ~spacing:5
      ~packing:vb#add ()
  in
802 803 804 805 806 807 808 809 810
  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
811
  let showattrs =
812
    GButton.check_button
813
      ~label:"show attributes in formulas"
814
      ~packing:display_options_box#add ()
815
      ~active:c.show_attributes
816 817
  in
  let (_ : GtkSignal.id) =
818
    showattrs#connect#toggled ~callback:
819
      (fun () ->
820 821
         c.show_attributes <- not c.show_attributes;
         set_attr_flag c.show_attributes)