gconfig.ml 20 KB
Newer Older
MARCHE Claude's avatar
MARCHE Claude committed
1 2
(**************************************************************************)
(*                                                                        *)
3
(*  Copyright (C) 2010-2011                                               *)
4 5 6
(*    François Bobot                                                      *)
(*    Jean-Christophe Filliâtre                                           *)
(*    Claude Marché                                                       *)
MARCHE Claude's avatar
MARCHE Claude committed
7 8 9 10 11 12 13 14 15 16 17 18
(*    Andrei Paskevich                                                    *)
(*                                                                        *)
(*  This software is free software; you can redistribute it and/or        *)
(*  modify it under the terms of the GNU Library General Public           *)
(*  License version 2.1, with the special exception on linking            *)
(*  described in file LICENSE.                                            *)
(*                                                                        *)
(*  This software is distributed in the hope that it will be useful,      *)
(*  but WITHOUT ANY WARRANTY; without even the implied warranty of        *)
(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.                  *)
(*                                                                        *)
(**************************************************************************)
MARCHE Claude's avatar
MARCHE Claude committed
19 20

open Format
21
open Why3
22
open Util
23
open Rc
24 25
open Whyconf

MARCHE Claude's avatar
MARCHE Claude committed
26

27 28
(* config file *)

29
type t =
MARCHE Claude's avatar
MARCHE Claude committed
30 31 32
    { mutable window_width : int;
      mutable window_height : int;
      mutable tree_width : int;
33
      mutable task_height : int;
34
      mutable time_limit : int;
35
      mutable mem_limit : int;
MARCHE Claude's avatar
MARCHE Claude committed
36
      mutable verbose : int;
37
      mutable max_running_processes : int;
38
      mutable default_editor : string;
39
      mutable intro_premises : bool;
MARCHE Claude's avatar
MARCHE Claude committed
40
      mutable show_labels : bool;
41
      mutable show_locs : bool;
MARCHE Claude's avatar
MARCHE Claude committed
42
      mutable show_time_limit : bool;
43
      mutable saving_policy : int;
44
      (** 0 = always, 1 = never, 2 = ask *)
Andrei Paskevich's avatar
minor  
Andrei Paskevich committed
45 46
      mutable premise_color : string;
      mutable goal_color : string;
47 48
      mutable error_color : string;
      (** colors *)
MARCHE Claude's avatar
MARCHE Claude committed
49
      mutable env : Env.env;
50
      mutable config : Whyconf.config;
MARCHE Claude's avatar
MARCHE Claude committed
51 52
    }

MARCHE Claude's avatar
MARCHE Claude committed
53

54 55 56 57 58 59
type ide = {
  ide_window_width : int;
  ide_window_height : int;
  ide_tree_width : int;
  ide_task_height : int;
  ide_verbose : int;
60 61 62
  ide_intro_premises : bool;
  ide_show_labels : bool;
  ide_show_locs : bool;
MARCHE Claude's avatar
MARCHE Claude committed
63
  ide_show_time_limit : bool;
64
  ide_saving_policy : int;
Andrei Paskevich's avatar
minor  
Andrei Paskevich committed
65 66
  ide_premise_color : string;
  ide_goal_color : string;
67
  ide_error_color : string;
68 69
  ide_default_editor : string;
}
MARCHE Claude's avatar
MARCHE Claude committed
70

71 72 73 74 75 76
let default_ide =
  { ide_window_width = 1024;
    ide_window_height = 768;
    ide_tree_width = 512;
    ide_task_height = 384;
    ide_verbose = 0;
77 78 79
    ide_intro_premises = true;
    ide_show_labels = false;
    ide_show_locs = false;
MARCHE Claude's avatar
MARCHE Claude committed
80
    ide_show_time_limit = false;
81
    ide_saving_policy = 0;
Andrei Paskevich's avatar
minor  
Andrei Paskevich committed
82 83
    ide_premise_color = "chartreuse";
    ide_goal_color = "gold";
84
    ide_error_color = "orange";
85 86 87
    ide_default_editor =
      try Sys.getenv "EDITOR" ^ " %f"
      with Not_found -> "editor %f";
88 89 90 91 92 93 94 95 96 97 98 99 100
  }

let load_ide section =
  { ide_window_width =
      get_int section ~default:default_ide.ide_window_width "window_width";
    ide_window_height =
      get_int section ~default:default_ide.ide_window_height "window_height";
    ide_tree_width =
      get_int section ~default:default_ide.ide_tree_width "tree_width";
    ide_task_height =
      get_int section ~default:default_ide.ide_task_height "task_height";
    ide_verbose =
      get_int section ~default:default_ide.ide_verbose "verbose";
101 102 103 104 105 106
    ide_intro_premises =
      get_bool section ~default:default_ide.ide_intro_premises "intro_premises";
    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
107 108
    ide_show_time_limit =
      get_bool section ~default:default_ide.ide_show_time_limit "print_time_limit";
109 110
    ide_saving_policy =
      get_int section ~default:default_ide.ide_saving_policy "saving_policy";
Andrei Paskevich's avatar
minor  
Andrei Paskevich committed
111 112 113 114 115 116
    ide_premise_color =
      get_string section ~default:default_ide.ide_premise_color
        "premise_color";
    ide_goal_color =
      get_string section ~default:default_ide.ide_goal_color
        "goal_color";
117 118 119
    ide_error_color =
      get_string section ~default:default_ide.ide_error_color
        "error_color";
120 121 122 123
    ide_default_editor =
      get_string section ~default:default_ide.ide_default_editor
        "default_editor";
  }
MARCHE Claude's avatar
MARCHE Claude committed
124

125 126 127 128 129 130 131 132 133 134 135

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

136
let load_config config =
137
  let main = get_main config in
138
  let ide  = match get_section config "ide" with
139 140
    | None -> default_ide
    | Some s -> load_ide s in
MARCHE Claude's avatar
MARCHE Claude committed
141
  (* temporary sets env to empty *)
142
  let env = Env.create_env [] in
143 144
  set_labels_flag ide.ide_show_labels;
  set_locs_flag ide.ide_show_locs;
MARCHE Claude's avatar
MARCHE Claude committed
145 146 147 148
  { window_height = ide.ide_window_height;
    window_width  = ide.ide_window_width;
    tree_width    = ide.ide_tree_width;
    task_height   = ide.ide_task_height;
149 150
    time_limit    = Whyconf.timelimit main;
    mem_limit     = Whyconf.memlimit main;
MARCHE Claude's avatar
MARCHE Claude committed
151
    verbose       = ide.ide_verbose;
152 153 154
    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
155
    show_time_limit = ide.ide_show_time_limit;
156
    saving_policy = ide.ide_saving_policy ;
Andrei Paskevich's avatar
minor  
Andrei Paskevich committed
157 158
    premise_color = ide.ide_premise_color;
    goal_color = ide.ide_goal_color;
159
    error_color = ide.ide_error_color;
160
    max_running_processes = Whyconf.running_provers_max main;
MARCHE Claude's avatar
MARCHE Claude committed
161 162 163 164
    default_editor = ide.ide_default_editor;
    config         = config;
    env            = env
  }
MARCHE Claude's avatar
MARCHE Claude committed
165

166
let save_config t =
167
  let _save_prover _ pr acc =
168
    Mstr.add pr.Session.prover_id
169
      {
170 171 172 173 174
        Whyconf.name    = pr.Session.prover_name;
        command = pr.Session.command;
        driver  = pr.Session.driver_name;
        version = pr.Session.prover_version;
        editor  = pr.Session.editor;
175
        interactive = pr.Session.interactive;
176 177
      } acc in
  let config = t.config in
178
  let config = set_main config
179 180 181
    (set_limits (get_main config)
       t.time_limit t.mem_limit t.max_running_processes)
  in
182 183 184 185 186 187
  let ide = empty_section in
  let ide = set_int ide "window_height" t.window_height in
  let ide = set_int ide "window_width" t.window_width in
  let ide = set_int ide "tree_width" t.tree_width in
  let ide = set_int ide "task_height" t.task_height in
  let ide = set_int ide "verbose" t.verbose in
188 189 190
  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
191
  let ide = set_bool ide "print_time_limit" t.show_time_limit in
192
  let ide = set_int ide "saving_policy" t.saving_policy in
Andrei Paskevich's avatar
minor  
Andrei Paskevich committed
193 194
  let ide = set_string ide "premise_color" t.premise_color in
  let ide = set_string ide "goal_color" t.goal_color in
195
  let ide = set_string ide "error_color" t.error_color in
196
  let ide = set_string ide "default_editor" t.default_editor in
197
  let config = set_section config "ide" ide in
198
(* TODO: store newly detected provers !
199
  let config = set_provers config
200
    (Mstr.fold save_prover t.provers Mstr.empty) in
201
*)
202
  save_config config
MARCHE Claude's avatar
MARCHE Claude committed
203

204 205 206 207 208 209 210 211 212 213 214 215 216 217 218 219 220 221 222
let read_config conf_file =
  try
    let config = Whyconf.read_config conf_file in
    load_config config
  with e when not (Debug.test_flag Debug.stack_trace) ->
    eprintf "@.%a@." Exn_printer.exn_printer e;
    exit 1

let config,read_config =
  let config = ref None in
  (fun () ->
    match !config with
      | None -> invalid_arg "configuration not yet loaded"
      | Some conf -> conf),
  (fun conf_file ->
    eprintf "[Info] reading IDE config file...@?";
    let c = read_config conf_file in
    eprintf " done.@.";
    config := Some c)
223

224
let save_config () = save_config (config ())
225

226
let get_main () = (get_main (config ()).config)
227 228


MARCHE Claude's avatar
MARCHE Claude committed
229 230
(*

MARCHE Claude's avatar
MARCHE Claude committed
231
  images, icons
MARCHE Claude's avatar
MARCHE Claude committed
232 233 234 235

*)

let image ?size f =
236
  let main = get_main () in
MARCHE Claude's avatar
MARCHE Claude committed
237
  let n = Filename.concat (datadir main) (Filename.concat "images" (f^".png"))
MARCHE Claude's avatar
MARCHE Claude committed
238 239 240 241 242 243 244
  in
  match size with
    | None ->
        GdkPixbuf.from_file n
    | Some s ->
        GdkPixbuf.from_file_at_size ~width:s ~height:s n

MARCHE Claude's avatar
MARCHE Claude committed
245 246
let iconname_default = "undone32"
let iconname_undone = "undone32"
247
let iconname_scheduled = "pausehalf32"
MARCHE Claude's avatar
MARCHE Claude committed
248 249 250 251 252 253
let iconname_running = "play32"
let iconname_valid = "accept32"
let iconname_unknown = "help32"
let iconname_invalid = "delete32"
let iconname_timeout = "clock32"
let iconname_failure = "bug32"
254 255 256 257 258
let iconname_valid_obs = "obsaccept32"
let iconname_unknown_obs = "obshelp32"
let iconname_invalid_obs = "obsdelete32"
let iconname_timeout_obs = "obsclock32"
let iconname_failure_obs = "obsbug32"
MARCHE Claude's avatar
MARCHE Claude committed
259 260 261 262 263
let iconname_yes = "accept32"
let iconname_no = "delete32"
let iconname_directory = "folder32"
let iconname_file = "file32"
let iconname_prover = "wizard32"
264
let iconname_transf = "configure32"
MARCHE Claude's avatar
MARCHE Claude committed
265
let iconname_editor = "edit32"
266
let iconname_replay = "refresh32"
267
let iconname_cancel = "cut32"
MARCHE Claude's avatar
MARCHE Claude committed
268
let iconname_reload = "movefile32"
MARCHE Claude's avatar
merge  
MARCHE Claude committed
269
let iconname_remove = "deletefile32"
270
let iconname_cleaning = "trashb32"
MARCHE Claude's avatar
MARCHE Claude committed
271

272
let image_default = ref (GdkPixbuf.create ~width:1 ~height:1 ()) (** dumb pixbuf *)
MARCHE Claude's avatar
MARCHE Claude committed
273
let image_undone = ref !image_default
MARCHE Claude's avatar
MARCHE Claude committed
274 275 276 277 278 279 280
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
let image_failure = ref !image_default
281 282 283 284 285
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
let image_failure_obs = ref !image_default
MARCHE Claude's avatar
MARCHE Claude committed
286 287 288 289 290 291
let image_yes = ref !image_default
let image_no = ref !image_default
let image_directory = ref !image_default
let image_file = ref !image_default
let image_prover = ref !image_default
let image_transf = ref !image_default
MARCHE Claude's avatar
MARCHE Claude committed
292
let image_editor = ref !image_default
293
let image_replay = ref !image_default
294
let image_cancel = ref !image_default
MARCHE Claude's avatar
MARCHE Claude committed
295
let image_reload = ref !image_default
MARCHE Claude's avatar
merge  
MARCHE Claude committed
296
let image_remove = ref !image_default
297
let image_cleaning = ref !image_default
MARCHE Claude's avatar
MARCHE Claude committed
298

MARCHE Claude's avatar
MARCHE Claude committed
299 300
let why_icon = ref !image_default

MARCHE Claude's avatar
MARCHE Claude committed
301 302
let resize_images size =
  image_default := image ~size iconname_default;
MARCHE Claude's avatar
MARCHE Claude committed
303
  image_undone := image ~size iconname_undone;
MARCHE Claude's avatar
MARCHE Claude committed
304 305 306 307 308 309 310
  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_failure := image ~size iconname_failure;
311 312 313 314 315
  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_failure_obs := image ~size iconname_failure_obs;
MARCHE Claude's avatar
MARCHE Claude committed
316 317 318 319 320 321
  image_yes := image ~size iconname_yes;
  image_no := image ~size iconname_no;
  image_directory := image ~size iconname_directory;
  image_file := image ~size iconname_file;
  image_prover := image ~size iconname_prover;
  image_transf := image ~size iconname_transf;
MARCHE Claude's avatar
MARCHE Claude committed
322
  image_editor := image ~size iconname_editor;
323
  image_replay := image ~size iconname_replay;
324
  image_cancel := image ~size iconname_cancel;
MARCHE Claude's avatar
MARCHE Claude committed
325
  image_reload := image ~size iconname_reload;
MARCHE Claude's avatar
merge  
MARCHE Claude committed
326
  image_remove := image ~size iconname_remove;
327
  image_cleaning := image ~size iconname_cleaning;
MARCHE Claude's avatar
MARCHE Claude committed
328 329
  ()

330
let init () =
331
  eprintf "[Info] reading icons...@?";
MARCHE Claude's avatar
MARCHE Claude committed
332
  why_icon := image "logo-why";
MARCHE Claude's avatar
MARCHE Claude committed
333 334
  resize_images 20;
  eprintf " done.@."
MARCHE Claude's avatar
MARCHE Claude committed
335 336

let show_legend_window () =
337
  let dialog = GWindow.dialog ~title:"Why3: legend of icons" () in
MARCHE Claude's avatar
MARCHE Claude committed
338
  let vbox = dialog#vbox in
339 340
  let text = GText.view ~packing:vbox#add
    ~editable:false ~cursor_visible:false () in
MARCHE Claude's avatar
MARCHE Claude committed
341
  let b = text#buffer in
342 343
  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
344
  let i s = b#insert ~iter:b#end_iter s in
345
  let it s = b#insert ~iter:b#end_iter ~tags:[tt] s in
MARCHE Claude's avatar
MARCHE Claude committed
346
  let ib i = b#insert_pixbuf ~iter:b#end_iter ~pixbuf:!i in
347
  it "Tree view\n";
MARCHE Claude's avatar
MARCHE Claude committed
348
  ib image_directory;
349
  i "   Theory, containing a set of goals\n";
MARCHE Claude's avatar
MARCHE Claude committed
350
  ib image_file;
351
  i "   Goal\n";
MARCHE Claude's avatar
MARCHE Claude committed
352
  ib image_prover;
353
  i "   External prover\n";
MARCHE Claude's avatar
MARCHE Claude committed
354
  ib image_transf;
MARCHE Claude's avatar
MARCHE Claude committed
355
  i "   Transformation\n";
356
  it "Status column\n";
MARCHE Claude's avatar
MARCHE Claude committed
357
  ib image_scheduled;
358
  i "   Scheduled external proof attempt\n";
MARCHE Claude's avatar
MARCHE Claude committed
359
  ib image_running;
360
  i "   Running external proof attempt\n";
MARCHE Claude's avatar
MARCHE Claude committed
361
  ib image_valid;
362 363 364 365 366
  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
367
  ib image_timeout;
368
  i "   External prover reached the time limit\n";
MARCHE Claude's avatar
MARCHE Claude committed
369
  ib image_unknown;
370
  i "   External prover answer not conclusive\n";
MARCHE Claude's avatar
MARCHE Claude committed
371
  ib image_failure;
372
  i "   External prover call failed\n";
MARCHE Claude's avatar
MARCHE Claude committed
373
  dialog#add_button "Close" `CLOSE ;
374 375
  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
376 377 378 379 380
  let ( _ : GWindow.Buttons.about) = dialog#run () in
  dialog#destroy ()


let show_about_window () =
MARCHE Claude's avatar
MARCHE Claude committed
381 382
  let about_dialog =
    GWindow.about_dialog
MARCHE Claude's avatar
MARCHE Claude committed
383
      ~name:"Why3"
MARCHE Claude's avatar
MARCHE Claude committed
384 385 386
      ~authors:["François Bobot";
                "Jean-Christophe Filliâtre";
                "Claude Marché";
MARCHE Claude's avatar
MARCHE Claude committed
387 388
                "Andrei Paskevich"
               ]
MARCHE Claude's avatar
MARCHE Claude committed
389
      ~copyright:"Copyright 2010-2011 Univ Paris-Sud, CNRS, INRIA"
390
      ~license:"GNU Lesser General Public License"
MARCHE Claude's avatar
MARCHE Claude committed
391 392 393
      ~website:"https://gforge.inria.fr/projects/why3"
      ~website_label:"Project web site"
      ~version:Config.version
MARCHE Claude's avatar
MARCHE Claude committed
394
      ()
MARCHE Claude's avatar
MARCHE Claude committed
395
  in
MARCHE Claude's avatar
MARCHE Claude committed
396 397
  let ( _ : GWindow.Buttons.about) = about_dialog#run () in
  about_dialog#destroy ()
MARCHE Claude's avatar
MARCHE Claude committed
398

399
let preferences c =
400
  let dialog = GWindow.dialog ~title:"Why3: preferences" () in
MARCHE Claude's avatar
MARCHE Claude committed
401 402
  let vbox = dialog#vbox in
  let notebook = GPack.notebook ~packing:vbox#add () in
403
  (** page 1 **)
MARCHE Claude's avatar
MARCHE Claude committed
404
  let label1 = GMisc.label ~text:"General" () in
MARCHE Claude's avatar
MARCHE Claude committed
405 406 407
  let page1 =
    GPack.vbox ~homogeneous:false ~packing:
      (fun w -> ignore(notebook#append_page ~tab_label:label1#coerce w)) ()
MARCHE Claude's avatar
MARCHE Claude committed
408
  in
409 410 411 412 413
  (* external processes frame *)
  let external_processes_frame =
    GBin.frame ~label:"External processes"
      ~packing:page1#add ()
  in
MARCHE Claude's avatar
MARCHE Claude committed
414
  (* editor *)
415 416
 let hb =
   GPack.hbox ~homogeneous:false ~packing:external_processes_frame#add ()
417
 in
418 419
 let _ =
   GMisc.label ~text:"Default editor: " ~packing:(hb#pack ~expand:false) ()
420
 in
421 422
 let editor_entry =
   GEdit.entry ~text:c.default_editor ~packing:hb#add ()
423
 in
MARCHE Claude's avatar
MARCHE Claude committed
424
 let (_ : GtkSignal.id) =
MARCHE Claude's avatar
MARCHE Claude committed
425 426 427
    editor_entry#connect#changed ~callback:
      (fun () -> c.default_editor <- editor_entry#text)
  in
428
  (* debug mode ? *)
MARCHE Claude's avatar
MARCHE Claude committed
429
(*
MARCHE Claude's avatar
MARCHE Claude committed
430
  let debugmode =
MARCHE Claude's avatar
MARCHE Claude committed
431
    GButton.check_button ~label:"debug" ~packing:page1#add ()
MARCHE Claude's avatar
MARCHE Claude committed
432 433
      ~active:(c.verbose > 0)
  in
MARCHE Claude's avatar
MARCHE Claude committed
434
  let (_ : GtkSignal.id) =
MARCHE Claude's avatar
MARCHE Claude committed
435 436
    debugmode#connect#toggled ~callback:
      (fun () -> c.verbose <- 1 - c.verbose)
MARCHE Claude's avatar
MARCHE Claude committed
437
  in
MARCHE Claude's avatar
MARCHE Claude committed
438
*)
439 440
  (* timelimit ? *)
  let hb = GPack.hbox ~homogeneous:false ~packing:page1#add () in
441
  let _ = GMisc.label ~text:"Time limit: " ~packing:(hb#pack ~expand:false) () in
442 443 444
  let timelimit_spin = GEdit.spin_button ~digits:0 ~packing:hb#add () in
  timelimit_spin#adjustment#set_bounds ~lower:2. ~upper:300. ~step_incr:1. ();
  timelimit_spin#adjustment#set_value (float_of_int c.time_limit);
MARCHE Claude's avatar
MARCHE Claude committed
445
  let (_ : GtkSignal.id) =
446 447 448 449
    timelimit_spin#connect#value_changed ~callback:
      (fun () -> c.time_limit <- timelimit_spin#value_as_int)
  in
  (* nb of processes ? *)
MARCHE Claude's avatar
MARCHE Claude committed
450
  let hb = GPack.hbox ~homogeneous:false ~packing:page1#add () in
451
  let _ = GMisc.label ~text:"Nb of processes: " ~packing:(hb#pack ~expand:false) () in
MARCHE Claude's avatar
MARCHE Claude committed
452
  let nb_processes_spin = GEdit.spin_button ~digits:0 ~packing:hb#add () in
453 454 455 456
  nb_processes_spin#adjustment#set_bounds
    ~lower:1. ~upper:16. ~step_incr:1. ();
  nb_processes_spin#adjustment#set_value
    (float_of_int c.max_running_processes);
MARCHE Claude's avatar
MARCHE Claude committed
457
  let (_ : GtkSignal.id) =
MARCHE Claude's avatar
MARCHE Claude committed
458
    nb_processes_spin#connect#value_changed ~callback:
459
      (fun () -> c.max_running_processes <- nb_processes_spin#value_as_int)
MARCHE Claude's avatar
MARCHE Claude committed
460
  in
461
  (** page 2 **)
462
  let label2 = GMisc.label ~text:"Colors" () in
463
  let _color_sel = GMisc.color_selection (* ~title:"Goal color" *)
464
    ~show:true
MARCHE Claude's avatar
MARCHE Claude committed
465 466
    ~packing:(fun w -> ignore(notebook#append_page
                                ~tab_label:label2#coerce w)) ()
MARCHE Claude's avatar
MARCHE Claude committed
467
  in
468 469 470 471 472 473 474
(*
  let (_ : GtkSignal.id) =
    color_sel#connect ColorSelection.S.color_changed ~callback:
      (fun _ -> Format.eprintf "Gconfig.color_sel : %s@."
         c)
  in
*)
475 476 477 478 479 480
  (** page 3 **)
  let label3 = GMisc.label ~text:"Provers" () in
  let _page3 = GMisc.label ~text:"This page should display detected provers"
    ~packing:(fun w -> ignore(notebook#append_page
                                ~tab_label:label3#coerce w)) ()
  in
481 482 483 484 485
  (** page 1 **)
  let display_options_frame =
    GBin.frame ~label:"Display options"
      ~packing:page1#add ()
  in
486
  (* options for task display *)
487 488 489 490
  let display_options_box =
    GPack.button_box `VERTICAL ~border_width:5 ~spacing:5
      ~packing:display_options_frame#add ()
  in
491 492 493 494 495 496 497 498 499
  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
500
  let showlabels =
501 502
    GButton.check_button
      ~label:"show labels in formulas"
503
      ~packing:display_options_box#add ()
504
      ~active:c.show_labels
505 506 507
  in
  let (_ : GtkSignal.id) =
    showlabels#connect#toggled ~callback:
508 509
      (fun () ->
         c.show_labels <- not c.show_labels;
510 511
         set_labels_flag c.show_labels)
  in
512
  let showlocs =
513 514
    GButton.check_button
      ~label:"show source locations in formulas"
515
      ~packing:display_options_box#add ()
516
      ~active:c.show_locs
517 518 519
  in
  let (_ : GtkSignal.id) =
    showlocs#connect#toggled ~callback:
520 521
      (fun () ->
         c.show_locs <- not c.show_locs;
522 523
         set_locs_flag c.show_locs)
  in
MARCHE Claude's avatar
MARCHE Claude committed
524 525 526 527 528 529 530 531 532 533 534
  let showtimelimit =
    GButton.check_button
      ~label:"show time limit for each proof"
      ~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
535
  let set_saving_policy n () = c.saving_policy <- n in
536
(*
537 538 539 540 541
  let label3 = GMisc.label ~text:"IDE" () in
  let page3 =
    GPack.vbox ~homogeneous:false ~packing:
      (fun w -> ignore(notebook#append_page ~tab_label:label3#coerce w)) ()
  in
542
*)
543
  (* session saving policy *)
544 545 546 547 548 549 550 551
  let saving_policy_frame =
    GBin.frame ~label:"Session saving policy"
      ~packing:page1#add ()
  in
  let saving_policy_box =
    GPack.button_box `VERTICAL ~border_width:5 ~spacing:5
      ~packing:saving_policy_frame#add ()
  in
552 553
  let choice0 =
    GButton.radio_button
554
      ~label:"always save on exit"
555
      ~active:(c.saving_policy = 0)
556
      ~packing:saving_policy_box#add ()
557 558 559
  in
  let choice1 =
    GButton.radio_button
560
      ~label:"never save on exit" ~group:choice0#group
561
      ~active:(c.saving_policy = 1)
562
      ~packing:saving_policy_box#add ()
563 564 565
  in
  let choice2 =
    GButton.radio_button
566 567
      ~label:"ask whether to save on exit" ~group:choice0#group
      ~active:(c.saving_policy = 2)
568
      ~packing:saving_policy_box#add ()
569
  in
570 571 572 573 574 575 576 577 578 579
  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
  (* buttons *)
MARCHE Claude's avatar
MARCHE Claude committed
580 581
  dialog#add_button "Close" `CLOSE ;
  let ( _ : GWindow.Buttons.about) = dialog#run () in
MARCHE Claude's avatar
MARCHE Claude committed
582
  eprintf "saving IDE config file@.";
583
  save_config ();
MARCHE Claude's avatar
MARCHE Claude committed
584
  dialog#destroy ()
585

586
(*
587
let run_auto_detection gconfig =
588 589
  let config = Autodetection.run_auto_detection gconfig.config in
  gconfig.config <- config;
590 591
  let _provers = get_provers config in
(* TODO: store the result differently
592 593
  gconfig.provers <- Mstr.fold (Session.get_prover_data gconfig.env) provers
  Mstr.empty
594 595
*)
  ()
596
*)
MARCHE Claude's avatar
MARCHE Claude committed
597

598 599 600
(* let () = eprintf "[Info] end of configuration initialization@." *)

let read_config conf_file = read_config conf_file; init ()
601

MARCHE Claude's avatar
MARCHE Claude committed
602
(*
MARCHE Claude's avatar
MARCHE Claude committed
603
Local Variables:
604
compile-command: "unset LANG; make -C ../.. bin/why3ide.byte"
MARCHE Claude's avatar
MARCHE Claude committed
605
End:
MARCHE Claude's avatar
MARCHE Claude committed
606
*)