Commit 5e82e6ce authored by MARCHE Claude's avatar MARCHE Claude
Browse files

Nicer look of preferences window

parent 71306d39
...@@ -54,12 +54,12 @@ ...@@ -54,12 +54,12 @@
* increment the magic number in config (A) * increment the magic number in config (A)
* remettre le use_api dans la doc (C) * put an up-to-date use_api.ml in the manual (C)
* deplacer le bouton "Cancel" dans le menu "tools", * deplacer le bouton "Cancel" dans le menu "tools",
le renommer en "make obsolete" et le documenter (A) le renommer en "make obsolete" et le documenter (A)
* documenter les options de Why (A) * document new Why options (A)
* Distribution of examples: we should distribute those who have an xml file * Distribution of examples: we should distribute those who have an xml file
under git, and distribute the XML and Coq proofs under git, and distribute the XML and Coq proofs
...@@ -70,6 +70,8 @@ ...@@ -70,6 +70,8 @@
* distribute bench files (A + F) * distribute bench files (A + F)
* document new IDE features (C)
* DONE enlever les caracteres de tab des sources * DONE enlever les caracteres de tab des sources
et les caracteres latin1 (A) et les caracteres latin1 (A)
......
...@@ -349,10 +349,21 @@ let preferences c = ...@@ -349,10 +349,21 @@ let preferences c =
GPack.vbox ~homogeneous:false ~packing: GPack.vbox ~homogeneous:false ~packing:
(fun w -> ignore(notebook#append_page ~tab_label:label1#coerce w)) () (fun w -> ignore(notebook#append_page ~tab_label:label1#coerce w)) ()
in in
(* external processes frame *)
let external_processes_frame =
GBin.frame ~label:"External processes"
~packing:page1#add ()
in
(* editor *) (* editor *)
let hb = GPack.hbox ~homogeneous:false ~packing:page1#add () in let hb =
let _ = GMisc.label ~text:"Default editor: " ~packing:(hb#pack ~expand:false) () in GPack.hbox ~homogeneous:false ~packing:external_processes_frame#add ()
let editor_entry = GEdit.entry ~text:c.default_editor ~packing:hb#add () in in
let _ =
GMisc.label ~text:"Default editor: " ~packing:(hb#pack ~expand:false) ()
in
let editor_entry =
GEdit.entry ~text:c.default_editor ~packing:hb#add ()
in
let (_ : GtkSignal.id) = let (_ : GtkSignal.id) =
editor_entry#connect#changed ~callback: editor_entry#connect#changed ~callback:
(fun () -> c.default_editor <- editor_entry#text) (fun () -> c.default_editor <- editor_entry#text)
...@@ -396,31 +407,61 @@ let preferences c = ...@@ -396,31 +407,61 @@ let preferences c =
~packing:(fun w -> ignore(notebook#append_page ~packing:(fun w -> ignore(notebook#append_page
~tab_label:label2#coerce w)) () ~tab_label:label2#coerce w)) ()
in in
(** page 3 **) (** page 1 **)
let display_options_frame =
GBin.frame ~label:"Display options"
~packing:page1#add ()
in
let display_options_box =
GPack.button_box `VERTICAL ~border_width:5 ~spacing:5
~packing:display_options_frame#add ()
in
(* toggle show labels in formulas *)
let showlabels =
GButton.check_button ~label:"show labels in formulas"
~packing:display_options_box#add ()
~active:(set_labels_flag c.show_labels;c.show_labels)
in
let (_ : GtkSignal.id) =
showlabels#connect#toggled ~callback:
(fun () -> c.show_labels <- not c.show_labels;
set_labels_flag c.show_labels)
in
let set_saving_policy n () = c.saving_policy <- n in let set_saving_policy n () = c.saving_policy <- n in
(*
let label3 = GMisc.label ~text:"IDE" () in let label3 = GMisc.label ~text:"IDE" () in
let page3 = let page3 =
GPack.vbox ~homogeneous:false ~packing: GPack.vbox ~homogeneous:false ~packing:
(fun w -> ignore(notebook#append_page ~tab_label:label3#coerce w)) () (fun w -> ignore(notebook#append_page ~tab_label:label3#coerce w)) ()
in in
*)
(* session saving policy *) (* session saving policy *)
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
let choice0 = let choice0 =
GButton.radio_button GButton.radio_button
~label:"Always save on exit" ~label:"Always save on exit"
~active:(c.saving_policy = 0) ~active:(c.saving_policy = 0)
~packing:page3#add () ~packing:saving_policy_box#add ()
in in
let choice1 = let choice1 =
GButton.radio_button GButton.radio_button
~label:"Never save on exit" ~group:choice0#group ~label:"Never save on exit" ~group:choice0#group
~active:(c.saving_policy = 1) ~active:(c.saving_policy = 1)
~packing:page3#add () ~packing:saving_policy_box#add ()
in in
let choice2 = let choice2 =
GButton.radio_button GButton.radio_button
~label:"ask whether to save on exit" ~group:choice0#group ~label:"ask whether to save on exit" ~group:choice0#group
~active:(c.saving_policy = 2) ~active:(c.saving_policy = 2)
~packing:page3#add () ~packing:saving_policy_box#add ()
in in
let (_ : GtkSignal.id) = let (_ : GtkSignal.id) =
choice0#connect#toggled ~callback:(set_saving_policy 0) choice0#connect#toggled ~callback:(set_saving_policy 0)
...@@ -431,16 +472,6 @@ let preferences c = ...@@ -431,16 +472,6 @@ let preferences c =
let (_ : GtkSignal.id) = let (_ : GtkSignal.id) =
choice2#connect#toggled ~callback:(set_saving_policy 2) choice2#connect#toggled ~callback:(set_saving_policy 2)
in in
(* toggle show labels in formulas *)
let showlabels =
GButton.check_button ~label:"show labels in formulas" ~packing:page3#add ()
~active:(set_labels_flag c.show_labels;c.show_labels)
in
let (_ : GtkSignal.id) =
showlabels#connect#toggled ~callback:
(fun () -> c.show_labels <- not c.show_labels;
set_labels_flag c.show_labels)
in
(* buttons *) (* buttons *)
dialog#add_button "Close" `CLOSE ; dialog#add_button "Close" `CLOSE ;
let ( _ : GWindow.Buttons.about) = dialog#run () in let ( _ : GWindow.Buttons.about) = dialog#run () in
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment