aboutsummaryrefslogtreecommitdiffhomepage
path: root/ide/preferences.ml
blob: f0fd45d77fb28e6ca8499ed3b062674f20862b1b (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
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
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
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
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
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
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
964
965
966
967
968
969
970
971
972
973
974
975
976
977
978
979
980
981
982
983
984
985
986
987
988
989
990
991
992
993
994
995
996
997
998
999
1000
1001
1002
1003
1004
1005
1006
1007
1008
1009
1010
1011
1012
1013
1014
1015
1016
1017
1018
1019
1020
1021
1022
1023
1024
1025
1026
1027
1028
1029
1030
1031
1032
(************************************************************************)
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
(*   \VV/  **************************************************************)
(*    //   *      This file is distributed under the terms of the       *)
(*         *       GNU Lesser General Public License Version 2.1        *)
(************************************************************************)

open Configwin

let pref_file = Filename.concat (Minilib.coqide_config_home ()) "coqiderc"
let accel_file = Filename.concat (Minilib.coqide_config_home ()) "coqide.keys"
let lang_manager = GSourceView2.source_language_manager ~default:true
let () = lang_manager#set_search_path
  ((Minilib.coqide_data_dirs ())@lang_manager#search_path)
let style_manager = GSourceView2.source_style_scheme_manager ~default:true
let () = style_manager#set_search_path
  ((Minilib.coqide_data_dirs ())@style_manager#search_path)

type tag = {
  tag_fg_color : string option;
  tag_bg_color : string option;
  tag_bold : bool;
  tag_italic : bool;
  tag_underline : bool;
}

(** Generic preferences *)

type obj = {
  set : string list -> unit;
  get : unit -> string list;
}

let preferences : obj Util.String.Map.t ref = ref Util.String.Map.empty
let unknown_preferences : string list Util.String.Map.t ref = ref Util.String.Map.empty

class type ['a] repr =
object
  method into : string list -> 'a option
  method from : 'a -> string list
end

class ['a] preference_signals ~(changed : 'a GUtil.signal) =
object
  inherit GUtil.ml_signals [changed#disconnect]
  method changed = changed#connect ~after
end

class ['a] preference ~(name : string list) ~(init : 'a) ~(repr : 'a repr) =
object (self)
  initializer
    let set v = match repr#into v with None -> () | Some s -> self#set s in
    let get () = repr#from self#get in
    let obj = { set = set; get = get; } in
    let name = String.concat "." name in
    if Util.String.Map.mem name !preferences then
      invalid_arg ("Preference " ^ name ^ " already exists")
    else
      preferences := Util.String.Map.add name obj !preferences

  val default = init
  val mutable data = init
  val changed : 'a GUtil.signal = new GUtil.signal ()
  val name : string list = name
  method connect = new preference_signals ~changed
  method get = data
  method set (n : 'a) = data <- n; changed#call n
  method reset () = self#set default
  method default = default
end

let stick (pref : 'a preference) (obj : #GObj.widget as 'obj)
  (cb : 'a -> unit) =
  let _ = cb pref#get in
  let p_id = pref#connect#changed (fun v -> cb v) in
  let _ = obj#misc#connect#destroy (fun () -> pref#connect#disconnect p_id) in
  ()

(** Useful marshallers *)

let mod_to_str m =
  match m with
    | `MOD1 -> "<Alt>"
    | `MOD2 -> "<Mod2>"
    | `MOD3 -> "<Mod3>"
    | `MOD4 -> "<Mod4>"
    | `MOD5 -> "<Mod5>"
    | `CONTROL -> "<Control>"
    | `SHIFT -> "<Shift>"
    | `HYPER -> "<Hyper>"
    | `META -> "<Meta>"
    | `RELEASE -> ""
    | `SUPER -> "<Super>"
    |  `BUTTON1| `BUTTON2| `BUTTON3| `BUTTON4| `BUTTON5| `LOCK -> ""

let mod_list_to_str l = List.fold_left (fun s m -> (mod_to_str m)^s) "" l

let str_to_mod_list s = snd (GtkData.AccelGroup.parse s)

type project_behavior = Ignore_args | Append_args | Subst_args

let string_of_project_behavior = function
  |Ignore_args -> "ignored"
  |Append_args -> "appended to arguments"
  |Subst_args -> "taken instead of arguments"

let project_behavior_of_string s =
  if s = "taken instead of arguments" then Subst_args
  else if s = "appended to arguments" then Append_args
  else Ignore_args

type inputenc = Elocale | Eutf8 | Emanual of string

let string_of_inputenc = function
  |Elocale -> "LOCALE"
  |Eutf8 -> "UTF-8"
  |Emanual s -> s

let inputenc_of_string s =
      (if s = "UTF-8" then Eutf8
       else if s = "LOCALE" then Elocale
       else Emanual s)

type line_ending = [ `DEFAULT | `WINDOWS | `UNIX ]

let line_end_of_string = function
| "unix" -> `UNIX
| "windows" -> `WINDOWS
| _ -> `DEFAULT

let line_end_to_string = function
| `UNIX -> "unix"
| `WINDOWS -> "windows"
| `DEFAULT -> "default"

let use_default_doc_url = "(automatic)"

module Repr =
struct

let string : string repr =
object
  method from s = [s]
  method into = function [s] -> Some s | _ -> None
end

let string_pair : (string * string) repr =
object
  method from (s1, s2) = [s1; s2]
  method into = function [s1; s2] -> Some (s1, s2) | _ -> None
end

let string_list : string list repr =
object
  method from s = s
  method into s = Some s
end

let string_pair_list (sep : char) : (string * string) list repr =
object
  val sep' = String.make 1 sep
  method from = CList.map (fun (s1, s2) -> CString.concat sep' [s1; s2])
  method into l =
    try
      Some (CList.map (fun s ->
        let split = CString.split sep s in
        CList.nth split 0, CList.nth split 1) l)
    with Failure _ -> None
end

let bool : bool repr =
object
  method from s = [string_of_bool s]
  method into = function
  | ["true"] -> Some true
  | ["false"] -> Some false
  | _ -> None
end

let int : int repr =
object
  method from s = [string_of_int s]
  method into = function
  | [i] -> (try Some (int_of_string i) with _ -> None)
  | _ -> None
end

let option (r : 'a repr) : 'a option repr =
object
  method from = function None -> [] | Some v -> "" :: r#from v
  method into = function
  | [] -> Some None
  | "" :: s -> Some (r#into s)
  | _ -> None
end

let custom (from : 'a -> string) (into : string -> 'a) : 'a repr =
object
  method from x = try [from x] with _ -> []
  method into = function
  | [s] -> (try Some (into s) with _ -> None)
  | _ -> None
end

let tag : tag repr =
let _to s = if s = "" then None else Some s in
let _of = function None -> "" | Some s -> s in
object
  method from tag = [
    _of tag.tag_fg_color;
    _of tag.tag_bg_color;
    string_of_bool tag.tag_bold;
    string_of_bool tag.tag_italic;
    string_of_bool tag.tag_underline;
  ]
  method into = function
  | [fg; bg; bd; it; ul] ->
    (try Some {
      tag_fg_color = _to fg;
      tag_bg_color = _to bg;
      tag_bold = bool_of_string bd;
      tag_italic = bool_of_string it;
      tag_underline = bool_of_string ul;
      }
    with _ -> None)
  | _ -> None
end

end

let get_config_file name =
  let find_config dir = Sys.file_exists (Filename.concat dir name) in
  let config_dir = List.find find_config (Minilib.coqide_config_dirs ()) in
  Filename.concat config_dir name

(* Small hack to handle v8.3 to v8.4 change in configuration file *)
let loaded_pref_file =
  try get_config_file "coqiderc"
  with Not_found -> Filename.concat (Option.default "" (Glib.get_home_dir ())) ".coqiderc"

let loaded_accel_file =
  try get_config_file "coqide.keys"
  with Not_found -> Filename.concat (Option.default "" (Glib.get_home_dir ())) ".coqide.keys"

(** Hooks *)

(** New style preferences *)

let cmd_coqtop =
  new preference ~name:["cmd_coqtop"] ~init:None ~repr:Repr.(option string)

let cmd_coqc =
  new preference ~name:["cmd_coqc"] ~init:"coqc" ~repr:Repr.(string)

let cmd_make =
  new preference ~name:["cmd_make"] ~init:"make" ~repr:Repr.(string)

let cmd_coqmakefile =
  new preference ~name:["cmd_coqmakefile"] ~init:"coq_makefile -o makefile *.v" ~repr:Repr.(string)

let cmd_coqdoc =
  new preference ~name:["cmd_coqdoc"] ~init:"coqdoc -q -g" ~repr:Repr.(string)

let source_language =
  new preference ~name:["source_language"] ~init:"coq" ~repr:Repr.(string)

let source_style =
  new preference ~name:["source_style"] ~init:"coq_style" ~repr:Repr.(string)

let global_auto_revert =
  new preference ~name:["global_auto_revert"] ~init:false ~repr:Repr.(bool)

let global_auto_revert_delay =
  new preference ~name:["global_auto_revert_delay"] ~init:10000 ~repr:Repr.(int)

let auto_save =
  new preference ~name:["auto_save"] ~init:true ~repr:Repr.(bool)

let auto_save_delay =
  new preference ~name:["auto_save_delay"] ~init:10000 ~repr:Repr.(int)

let auto_save_name =
  new preference ~name:["auto_save_name"] ~init:("#","#") ~repr:Repr.(string_pair)

let read_project =
  let repr = Repr.custom string_of_project_behavior project_behavior_of_string in
  new preference ~name:["read_project"] ~init:Append_args ~repr

let project_file_name =
  new preference ~name:["project_file_name"] ~init:"_CoqProject" ~repr:Repr.(string)

let project_path =
  new preference ~name:["project_path"] ~init:None ~repr:Repr.(option string)

let encoding =
  let repr = Repr.custom string_of_inputenc inputenc_of_string in
  let init = if Sys.os_type = "Win32" then Eutf8 else Elocale in
  new preference ~name:["encoding"] ~init ~repr

let automatic_tactics =
  let init = ["trivial"; "tauto"; "auto"; "omega"; "auto with *"; "intuition" ] in
  new preference ~name:["automatic_tactics"] ~init ~repr:Repr.(string_list)

let cmd_print =
  new preference ~name:["cmd_print"] ~init:"lpr" ~repr:Repr.(string)

let attach_modifiers (pref : string preference) prefix =
  let cb mds =
    let mds = str_to_mod_list mds in
    let change ~path ~key ~modi ~changed =
      if CString.is_sub prefix path 0 then
        ignore (GtkData.AccelMap.change_entry ~key ~modi:mds ~replace:true path)
    in
    GtkData.AccelMap.foreach change
  in
  pref#connect#changed cb

let modifier_for_navigation =
  new preference ~name:["modifier_for_navigation"] ~init:"<Control>" ~repr:Repr.(string)

let modifier_for_templates =
  new preference ~name:["modifier_for_templates"] ~init:"<Control><Shift>" ~repr:Repr.(string)
 
let modifier_for_tactics =
  new preference ~name:["modifier_for_tactics"] ~init:"<Control><Alt>" ~repr:Repr.(string)

let modifier_for_display =
  new preference ~name:["modifier_for_display"] ~init:"<Alt><Shift>" ~repr:Repr.(string)

let modifier_for_queries =
  new preference ~name:["modifier_for_queries"] ~init:"<Control><Shift>" ~repr:Repr.(string)

let _ = attach_modifiers modifier_for_navigation "<Actions>/Navigation/"
let _ = attach_modifiers modifier_for_templates "<Actions>/Templates/"
let _ = attach_modifiers modifier_for_tactics "<Actions>/Tactics/"
let _ = attach_modifiers modifier_for_display "<Actions>/View/"
let _ = attach_modifiers modifier_for_queries "<Actions>/Queries/"

let modifiers_valid =
  new preference ~name:["modifiers_valid"] ~init:"<Alt><Control><Shift>" ~repr:Repr.(string)

let cmd_browse =
  new preference ~name:["cmd_browse"] ~init:Flags.browser_cmd_fmt ~repr:Repr.(string)

let cmd_editor =
  let init = if Sys.os_type = "Win32" then "NOTEPAD %s" else "emacs %s" in
  new preference ~name:["cmd_editor"] ~init ~repr:Repr.(string)

let text_font =
  let init = match Coq_config.gtk_platform with
  | `QUARTZ -> "Arial Unicode MS 11"
  | _ -> "Monospace 10"
  in
  new preference ~name:["text_font"] ~init ~repr:Repr.(string)

let doc_url =
object
  inherit [string] preference
    ~name:["doc_url"] ~init:Coq_config.wwwrefman ~repr:Repr.(string)
    as super

  method set v =
    if not (Flags.is_standard_doc_url v) &&
      v <> use_default_doc_url &&
      (* Extra hack to support links to last released doc version *)
      v <> Coq_config.wwwcoq ^ "doc" &&
      v <> Coq_config.wwwcoq ^ "doc/"
    then super#set v

end

let library_url =
  new preference ~name:["library_url"] ~init:Coq_config.wwwstdlib ~repr:Repr.(string)

let show_toolbar =
  new preference ~name:["show_toolbar"] ~init:true ~repr:Repr.(bool)

let contextual_menus_on_goal =
  new preference ~name:["contextual_menus_on_goal"] ~init:true ~repr:Repr.(bool)

let window_width =
  new preference ~name:["window_width"] ~init:800 ~repr:Repr.(int)

let window_height =
  new preference ~name:["window_height"] ~init:600 ~repr:Repr.(int)

let auto_complete =
  new preference ~name:["auto_complete"] ~init:false ~repr:Repr.(bool)

let stop_before =
  new preference ~name:["stop_before"] ~init:true ~repr:Repr.(bool)

let reset_on_tab_switch =
  new preference ~name:["reset_on_tab_switch"] ~init:false ~repr:Repr.(bool)

let line_ending =
  let repr = Repr.custom line_end_to_string line_end_of_string in
  new preference ~name:["line_ending"] ~init:`DEFAULT ~repr

let vertical_tabs =
  new preference ~name:["vertical_tabs"] ~init:false ~repr:Repr.(bool)

let opposite_tabs =
  new preference ~name:["opposite_tabs"] ~init:false ~repr:Repr.(bool)

let background_color =
  new preference ~name:["background_color"] ~init:"cornsilk" ~repr:Repr.(string)

let attach_bg (pref : string preference) (tag : GText.tag) =
  pref#connect#changed (fun c -> tag#set_property (`BACKGROUND c))

let attach_fg (pref : string preference) (tag : GText.tag) =
  pref#connect#changed (fun c -> tag#set_property (`FOREGROUND c))

let processing_color =
  new preference ~name:["processing_color"] ~init:"light blue" ~repr:Repr.(string)

let _ = attach_bg processing_color Tags.Script.to_process
let _ = attach_bg processing_color Tags.Script.incomplete

let tags = ref Util.String.Map.empty

let list_tags () = !tags

let make_tag ?fg ?bg ?(bold = false) ?(italic = false) ?(underline = false) () = {
  tag_fg_color = fg;
  tag_bg_color = bg;
  tag_bold = bold;
  tag_italic = italic;
  tag_underline = underline;
}

let create_tag name default =
  let pref = new preference ~name:[name] ~init:default ~repr:Repr.(tag) in
  let set_tag tag =
    begin match pref#get.tag_bg_color with
    | None -> tag#set_property (`BACKGROUND_SET false)
    | Some c ->
      tag#set_property (`BACKGROUND_SET true);
      tag#set_property (`BACKGROUND c)
    end;
    begin match pref#get.tag_fg_color with
    | None -> tag#set_property (`FOREGROUND_SET false)
    | Some c ->
      tag#set_property (`FOREGROUND_SET true);
      tag#set_property (`FOREGROUND c)
    end;
    begin match pref#get.tag_bold with
    | false -> tag#set_property (`WEIGHT_SET false)
    | true ->
      tag#set_property (`WEIGHT_SET true);
      tag#set_property (`WEIGHT `BOLD)
    end;
    begin match pref#get.tag_italic with
    | false -> tag#set_property (`STYLE_SET false)
    | true ->
      tag#set_property (`STYLE_SET true);
      tag#set_property (`STYLE `ITALIC)
    end;
    begin match pref#get.tag_underline with
    | false -> tag#set_property (`UNDERLINE_SET false)
    | true ->
      tag#set_property (`UNDERLINE_SET true);
      tag#set_property (`UNDERLINE `SINGLE)
    end;
  in
  let iter table =
    let tag = GText.tag ~name () in
    table#add tag#as_tag;
    ignore (pref#connect#changed (fun _ -> set_tag tag));
    set_tag tag;
  in
  List.iter iter [Tags.Script.table; Tags.Proof.table; Tags.Message.table];
  tags := Util.String.Map.add name pref !tags

let () =
  let iter (name, tag) = create_tag name tag in
  List.iter iter [
    ("constr.evar", make_tag ());
    ("constr.keyword", make_tag ~fg:"dark green" ());
    ("constr.notation", make_tag ());
    ("constr.path", make_tag ());
    ("constr.reference", make_tag ~fg:"navy"());
    ("constr.type", make_tag ~fg:"#008080" ());
    ("constr.variable", make_tag ());
    ("message.debug", make_tag ());
    ("message.error", make_tag ());
    ("message.warning", make_tag ());
    ("module.definition", make_tag ~fg:"orange red" ~bold:true ());
    ("module.keyword", make_tag ());
    ("tactic.keyword", make_tag ());
    ("tactic.primitive", make_tag ());
    ("tactic.string", make_tag ());
  ]

let processed_color =
  new preference ~name:["processed_color"] ~init:"light green" ~repr:Repr.(string)

let _ = attach_bg processed_color Tags.Script.processed
let _ = attach_bg processed_color Tags.Proof.highlight

let error_color =
  new preference ~name:["error_color"] ~init:"#FFCCCC" ~repr:Repr.(string)

let _ = attach_bg error_color Tags.Script.error_bg

let error_fg_color =
  new preference ~name:["error_fg_color"] ~init:"red" ~repr:Repr.(string)

let _ = attach_fg error_fg_color Tags.Script.error

let dynamic_word_wrap =
  new preference ~name:["dynamic_word_wrap"] ~init:false ~repr:Repr.(bool)

let show_line_number =
  new preference ~name:["show_line_number"] ~init:false ~repr:Repr.(bool)

let auto_indent =
  new preference ~name:["auto_indent"] ~init:false ~repr:Repr.(bool)

let show_spaces =
  new preference ~name:["show_spaces"] ~init:true ~repr:Repr.(bool)

let show_right_margin =
  new preference ~name:["show_right_margin"] ~init:false ~repr:Repr.(bool)

let show_progress_bar =
  new preference ~name:["show_progress_bar"] ~init:true ~repr:Repr.(bool)

let spaces_instead_of_tabs =
  new preference ~name:["spaces_instead_of_tabs"] ~init:true ~repr:Repr.(bool)

let tab_length =
  new preference ~name:["tab_length"] ~init:2 ~repr:Repr.(int)

let highlight_current_line =
  new preference ~name:["highlight_current_line"] ~init:false ~repr:Repr.(bool)

let nanoPG =
  new preference ~name:["nanoPG"] ~init:false ~repr:Repr.(bool)

let user_queries =
  new preference ~name:["user_queries"] ~init:[] ~repr:Repr.(string_pair_list '$')

class tag_button (box : Gtk.box Gtk.obj) =
object (self)

  inherit GObj.widget box

  val fg_color = GButton.color_button ()
  val fg_unset = GButton.toggle_button ()
  val bg_color = GButton.color_button ()
  val bg_unset = GButton.toggle_button ()
  val bold = GButton.toggle_button ()
  val italic = GButton.toggle_button ()
  val underline = GButton.toggle_button ()

  method set_tag tag =
    let track c but set = match c with
    | None -> set#set_active true
    | Some c ->
      set#set_active false;
      but#set_color (Tags.color_of_string c)
    in
    track tag.tag_bg_color bg_color bg_unset;
    track tag.tag_fg_color fg_color fg_unset;
    bold#set_active tag.tag_bold;
    italic#set_active tag.tag_italic;
    underline#set_active tag.tag_underline;

  method tag =
    let get but set =
      if set#active then None
      else Some (Tags.string_of_color but#color)
    in
    {
      tag_bg_color = get bg_color bg_unset;
      tag_fg_color = get fg_color fg_unset;
      tag_bold = bold#active;
      tag_italic = italic#active;
      tag_underline = underline#active;
    }

  initializer
    let box = new GPack.box box in
    let set_stock button stock =
      let stock = GMisc.image ~stock ~icon_size:`BUTTON () in
      button#set_image stock#coerce
    in
    set_stock fg_unset `CANCEL;
    set_stock bg_unset `CANCEL;
    set_stock bold `BOLD;
    set_stock italic `ITALIC;
    set_stock underline `UNDERLINE;
    box#pack fg_color#coerce;
    box#pack fg_unset#coerce;
    box#pack bg_color#coerce;
    box#pack bg_unset#coerce;
    box#pack bold#coerce;
    box#pack italic#coerce;
    box#pack underline#coerce;
    let cb but obj = obj#set_sensitive (not but#active) in
    let _ = fg_unset#connect#toggled (fun () -> cb fg_unset fg_color#misc) in
    let _ = bg_unset#connect#toggled (fun () -> cb bg_unset bg_color#misc) in
    ()

end

let tag_button () =
  let box = GPack.hbox () in
  new tag_button (Gobject.unsafe_cast box#as_widget)

(** Old style preferences *)

let save_pref () =
  if not (Sys.file_exists (Minilib.coqide_config_home ()))
  then Unix.mkdir (Minilib.coqide_config_home ()) 0o700;
  let () = try GtkData.AccelMap.save accel_file with _ -> () in
  let add = Util.String.Map.add in
  let fold key obj accu = add key (obj.get ()) accu in
  let prefs = Util.String.Map.fold fold !preferences Util.String.Map.empty in
  let prefs = Util.String.Map.fold Util.String.Map.add !unknown_preferences prefs in
  Config_lexer.print_file pref_file prefs

let load_pref () =
  let () = try GtkData.AccelMap.load loaded_accel_file with _ -> () in

    let m = Config_lexer.load_file loaded_pref_file in
    let iter name v =
      if Util.String.Map.mem name !preferences then
        try (Util.String.Map.find name !preferences).set v with _ -> ()
      else unknown_preferences := Util.String.Map.add name v !unknown_preferences
    in
    Util.String.Map.iter iter m

let pstring name p = string ~f:p#set name p#get
let pbool name p = bool ~f:p#set name p#get
let pmodifiers ?(all = false) name p = modifiers
  ?allow:(if all then None else Some (str_to_mod_list modifiers_valid#get))
  ~f:(fun l -> p#set (mod_list_to_str l))
  ~help:"restart to apply"
  name
  (str_to_mod_list p#get)

let configure ?(apply=(fun () -> ())) () =
  let cmd_coqtop =
    string
      ~f:(fun s -> cmd_coqtop#set (if s = "AUTO" then None else Some s))
      "       coqtop" (match cmd_coqtop#get with |None -> "AUTO" | Some x -> x) in
  let cmd_coqc = pstring "       coqc" cmd_coqc in
  let cmd_make = pstring "       make" cmd_make in
  let cmd_coqmakefile = pstring "coqmakefile" cmd_coqmakefile in
  let cmd_coqdoc = pstring "     coqdoc" cmd_coqdoc in
  let cmd_print = pstring "   Print ps" cmd_print in

  let config_font =
    let box = GPack.hbox () in
    let w = GMisc.font_selection () in
    w#set_preview_text
      "Goal (∃n : nat, n ≤ 0)∧(∀x,y,z, x∈y⋃z↔x∈y∨x∈z).";
    box#pack ~expand:true w#coerce;
    ignore (w#misc#connect#realize
	      ~callback:(fun () -> w#set_font_name text_font#get));
    custom
      ~label:"Fonts for text"
      box
      (fun () ->
	 let fd =  w#font_name in
	 text_font#set fd)
      true
  in

  let config_color =
    let box = GPack.vbox () in
    let table = GPack.table
      ~row_spacings:5
      ~col_spacings:5
      ~border_width:2
      ~packing:(box#pack ~expand:true) ()
    in
    let reset_button = GButton.button
      ~label:"Reset"
      ~packing:box#pack ()
    in
    let iter i (text, pref) =
      let label = GMisc.label
        ~text ~packing:(table#attach ~expand:`X ~left:0 ~top:i) ()
      in
      let () = label#set_xalign 0. in
      let button = GButton.color_button
        ~color:(Tags.color_of_string pref#get)
        ~packing:(table#attach ~left:1 ~top:i) ()
      in
      let _ = button#connect#color_set begin fun () ->
        pref#set (Tags.string_of_color button#color)
      end in
      let reset _ =
        pref#reset ();
        button#set_color Tags.(color_of_string pref#get)
      in
      let _ = reset_button#connect#clicked ~callback:reset in
      ()
    in
    let () = Util.List.iteri iter [
      ("Background color", background_color);
      ("Background color of processed text", processed_color);
      ("Background color of text being processed", processing_color);
      ("Background color of errors", error_color);
      ("Foreground color of errors", error_fg_color);
    ] in
    let label = "Color configuration" in
    let callback () = () in
    custom ~label box callback true
  in

  let config_tags =
    let box = GPack.vbox () in
    let scroll = GBin.scrolled_window
      ~hpolicy:`NEVER
      ~vpolicy:`AUTOMATIC
      ~packing:(box#pack ~expand:true)
      ()
    in
    let table = GPack.table
      ~row_spacings:5
      ~col_spacings:5
      ~border_width:2
      ~packing:scroll#add_with_viewport ()
    in
    let i = ref 0 in
    let cb = ref [] in
    let iter text tag =
      let label = GMisc.label
        ~text ~packing:(table#attach ~expand:`X ~left:0 ~top:!i) ()
      in
      let () = label#set_xalign 0. in
      let button = tag_button () in
      let callback () = tag#set button#tag in
      button#set_tag tag#get;
      table#attach ~left:1 ~top:!i button#coerce;
      incr i;
      cb := callback :: !cb;
    in
    let () = Util.String.Map.iter iter !tags in
    let label = "Tag configuration" in
    let callback () = List.iter (fun f -> f ()) !cb in
    custom ~label box callback true
  in

  let config_editor =
    let label = "Editor configuration" in
    let box = GPack.vbox () in
    let button text (pref : bool preference) =
      let active = pref#get in
      let but = GButton.check_button ~label:text ~active ~packing:box#pack () in
      ignore (but#connect#toggled (fun () -> pref#set but#active))
    in
    let () = button "Dynamic word wrap" dynamic_word_wrap in
    let () = button "Show line number" show_line_number in
    let () = button "Auto indentation" auto_indent in
    let () = button "Auto completion" auto_complete in
    let () = button "Show spaces" show_spaces in
    let () = button "Show right margin" show_right_margin in
    let () = button "Show progress bar" show_progress_bar in
    let () = button "Insert spaces instead of tabs" spaces_instead_of_tabs in
    let () = button "Highlight current line" highlight_current_line in
    let () = button "Emacs/PG keybindings (μPG mode)" nanoPG in
    let callback () = () in
    custom ~label box callback true
  in

(*
  let show_toolbar =
    bool
      ~f:(fun s ->
	    current.show_toolbar <- s;
	    !show_toolbar s)
      "Show toolbar" current.show_toolbar
  in
  let window_height =
    string
    ~f:(fun s -> current.window_height <- (try int_of_string s with _ -> 600);
	  !resize_window ();
       )
      "Window height"
      (string_of_int current.window_height)
  in
  let window_width =
    string
    ~f:(fun s -> current.window_width <-
	  (try int_of_string s with _ -> 800))
      "Window width"
      (string_of_int current.window_width)
  in
*)
(*
  let config_appearance = [show_toolbar; window_width; window_height] in
*)
  let global_auto_revert = pbool "Enable global auto revert" global_auto_revert in
  let global_auto_revert_delay =
    string
    ~f:(fun s -> global_auto_revert_delay#set
	  (try int_of_string s with _ -> 10000))
      "Global auto revert delay (ms)"
      (string_of_int global_auto_revert_delay#get)
  in

  let auto_save = pbool "Enable auto save" auto_save in
  let auto_save_delay =
    string
    ~f:(fun s -> auto_save_delay#set
	  (try int_of_string s with _ -> 10000))
      "Auto save delay (ms)"
      (string_of_int auto_save_delay#get)
  in

  let stop_before = pbool "Stop interpreting before the current point" stop_before in

  let reset_on_tab_switch = pbool "Reset coqtop on tab switch" reset_on_tab_switch in

  let vertical_tabs = pbool "Vertical tabs" vertical_tabs in

  let opposite_tabs = pbool "Tabs on opposite side" opposite_tabs in

  let encodings =
    combo
      "File charset encoding "
      ~f:(fun s -> encoding#set (inputenc_of_string s))
      ~new_allowed: true
      ("UTF-8"::"LOCALE":: match encoding#get with
	|Emanual s -> [s]
	|_ -> []
      )
      (string_of_inputenc encoding#get)
  in

  let line_ending =
    combo
      "EOL character"
      ~f:(fun s -> line_ending#set (line_end_of_string s))
      ~new_allowed:false
      ["unix"; "windows"; "default"]
      (line_end_to_string line_ending#get)
  in

  let source_style =
    combo "Highlighting style:"
      ~f:source_style#set ~new_allowed:false
      style_manager#style_scheme_ids source_style#get
  in

  let source_language =
    combo "Language:"
      ~f:source_language#set ~new_allowed:false
      (List.filter
        (fun x -> Str.string_match (Str.regexp "^coq") x 0)
        lang_manager#language_ids)
      source_language#get
  in

  let read_project =
    combo
      "Project file options are"
      ~f:(fun s -> read_project#set (project_behavior_of_string s))
      ~editable:false
      [string_of_project_behavior Subst_args;
       string_of_project_behavior Append_args;
       string_of_project_behavior Ignore_args]
      (string_of_project_behavior read_project#get)
  in
  let project_file_name = pstring "Default name for project file" project_file_name in
  let modifier_for_tactics =
    pmodifiers "Modifiers for Tactics Menu" modifier_for_tactics
  in
  let modifier_for_templates =
    pmodifiers "Modifiers for Templates Menu" modifier_for_templates
  in
  let modifier_for_navigation =
    pmodifiers "Modifiers for Navigation Menu" modifier_for_navigation
  in
  let modifier_for_display =
    pmodifiers "Modifiers for View Menu" modifier_for_display
  in
  let modifier_for_queries =
    pmodifiers "Modifiers for Queries Menu" modifier_for_queries
  in
  let modifiers_valid =
    pmodifiers ~all:true "Allowed modifiers" modifiers_valid
  in
  let cmd_editor =
    let predefined = [ "emacs %s"; "vi %s"; "NOTEPAD %s" ] in
    combo
      ~help:"(%s for file name)"
      "External editor"
      ~f:cmd_editor#set
      ~new_allowed: true
      (predefined@[if List.mem cmd_editor#get predefined then ""
                   else cmd_editor#get])
      cmd_editor#get
  in
  let cmd_browse =
    let predefined = [
      Coq_config.browser;
      "netscape -remote \"openURL(%s)\"";
      "mozilla -remote \"openURL(%s)\"";
      "firefox -remote \"openURL(%s,new-windows)\" || firefox %s &";
      "seamonkey -remote \"openURL(%s)\" || seamonkey %s &"
    ] in
    combo
      ~help:"(%s for url)"
      "Browser"
      ~f:cmd_browse#set
      ~new_allowed: true
      (predefined@[if List.mem cmd_browse#get predefined then ""
                   else cmd_browse#get])
      cmd_browse#get
  in
  let doc_url =
    let predefined = [
      "file://"^(List.fold_left Filename.concat (Coq_config.docdir) ["refman";"html"]);
      Coq_config.wwwrefman;
      use_default_doc_url
    ] in
    combo
      "Manual URL"
      ~f:doc_url#set
      ~new_allowed: true
      (predefined@[if List.mem doc_url#get predefined then ""
                   else doc_url#get])
      doc_url#get in
  let library_url =
    let predefined = [
      "file://"^(List.fold_left Filename.concat (Coq_config.docdir) ["stdlib";"html"]);
      Coq_config.wwwstdlib
    ] in
    combo
      "Library URL"
      ~f:(fun s -> library_url#set s)
      ~new_allowed: true
      (predefined@[if List.mem library_url#get predefined then ""
                   else library_url#get])
      library_url#get
  in
  let automatic_tactics =
    strings
      ~f:automatic_tactics#set
      ~add:(fun () -> ["<edit me>"])
      "Wizard tactics to try in order"
      automatic_tactics#get

  in

  let contextual_menus_on_goal = pbool "Contextual menus on goal" contextual_menus_on_goal in

  let misc = [contextual_menus_on_goal;stop_before;reset_on_tab_switch;
              vertical_tabs;opposite_tabs] in

  let add_user_query () =
    let input_string l v =
      match GToolbox.input_string ~title:l v with
      | None -> ""
      | Some s -> s
    in
    let q = input_string "User query" "Your query" in
    let k = input_string "Shortcut key" "Shortcut (a single letter)" in
    let q = CString.map (fun c -> if c = '$' then ' ' else c) q in
    (* Anything that is not a simple letter will be ignored. *)
    let k =
      if Int.equal (CString.length k) 1 && Util.is_letter k.[0] then k
      else "" in
    let k = CString.uppercase k in
      [q, k]
  in

  let user_queries =
    list
      ~f:user_queries#set
      (* Disallow same query, key or empty query. *)
      ~eq:(fun (q1, k1) (q2, k2) -> k1 = k2 || q1 = "" || q2 = "" || q1 = q2)
      ~add:add_user_query
      ~titles:["User query"; "Shortcut key"]
      "User queries"
      (fun (q, s) -> [q; s])
      user_queries#get

  in

(* ATTENTION !!!!! L'onglet Fonts doit etre en premier pour eviter un bug !!!!
   (shame on Benjamin) *)
  let cmds =
    [Section("Fonts", Some `SELECT_FONT,
	     [config_font]);
     Section("Colors", Some `SELECT_COLOR,
             [config_color; source_language; source_style]);
     Section("Tags", Some `SELECT_COLOR,
             [config_tags]);
     Section("Editor", Some `EDIT, [config_editor]);
     Section("Files", Some `DIRECTORY,
	     [global_auto_revert;global_auto_revert_delay;
	      auto_save; auto_save_delay; (* auto_save_name*)
	      encodings; line_ending;
	     ]);
     Section("Project", Some (`STOCK "gtk-page-setup"),
	     [project_file_name;read_project;
	     ]);
(*
     Section("Appearance",
	     config_appearance);
*)
     Section("Externals", None,
	     [cmd_coqtop;cmd_coqc;cmd_make;cmd_coqmakefile; cmd_coqdoc;
	      cmd_print;cmd_editor;cmd_browse;doc_url;library_url]);
     Section("Tactics Wizard", None,
	     [automatic_tactics]);
     Section("Shortcuts", Some `PREFERENCES,
	     [modifiers_valid; modifier_for_tactics;
        modifier_for_templates; modifier_for_display; modifier_for_navigation;
        modifier_for_queries; user_queries]);
     Section("Misc", Some `ADD,
       misc)]
  in
(*
  Format.printf "before edit: current.text_font = %s@." (Pango.Font.to_string current.text_font);
*)
  let x = edit ~apply "Customizations" cmds in
(*
  Format.printf "after edit: current.text_font = %s@." (Pango.Font.to_string current.text_font);
*)
  match x with
    | Return_apply | Return_ok -> save_pref ()
    | Return_cancel -> ()