Some improvements in the settings window

diff --git a/helm/interface/mmlinterface.ml b/helm/interface/mmlinterface.ml
index 784c9f4b127e47a21089047296af4dc079675dfa..cfccfbb3f18b8b38de75f406b2677f567d7546ff 100755 (executable)
--- a/helm/interface/mmlinterface.ml
+++ b/helm/interface/mmlinterface.ml
@@ -428,27 +428,46 @@ let export_to_postscript output () =
  !output#export_to_postscript "output.ps" ;
 ;;
 
-let activate_t1 output sw is_set jump_callback selection_changed_callback 
- last_uri ()
+let activate_t1 output button_set_anti_aliasing button_set_kerning 
+ button_export_to_postscript sw button_t1 jump_callback
+ selection_changed_callback last_uri ()
 =
- is_set := not !is_set ;
- sw#remove !output#coerce ;
- output :=
- (GMathView.math_view ~packing:sw#add ~width:400 ~height:380
-  ~use_t1_lib:!is_set ()) ;
- !output#load !last_uri ;
- ignore(!output#connect#jump jump_callback) ;
- ignore(!output#connect#selection_changed selection_changed_callback) ;
-;;
-
-let set_anti_aliasing output is_set () =
- is_set := not !is_set ;
- !output#set_anti_aliasing !is_set
-;;
-
-let set_kerning output is_set () =
- is_set := not !is_set ;
- !output#set_kerning !is_set
+ let is_set = button_t1#active in
+  sw#remove !output#coerce ;
+  let font_size = !output#get_font_size in
+  let log_verbosity = !output#get_log_verbosity in
+  let anti_aliasing = button_set_anti_aliasing#active in
+  let kerning = button_set_kerning#active in
+   output :=
+   (GMathView.math_view ~packing:sw#add ~width:400 ~height:380
+    ~use_t1_lib:is_set ()) ;
+   !output#set_font_size font_size ;
+   !output#set_log_verbosity log_verbosity ;
+   if is_set then
+    begin
+     button_set_anti_aliasing#misc#set_sensitive true ;
+     button_set_kerning#misc#set_sensitive true ;
+     button_export_to_postscript#misc#set_sensitive true ;
+     !output#set_anti_aliasing anti_aliasing ;
+     !output#set_kerning kerning ;
+    end
+   else
+    begin
+     button_set_anti_aliasing#misc#set_sensitive false ;
+     button_set_kerning#misc#set_sensitive false ;
+     button_export_to_postscript#misc#set_sensitive false ;
+    end ;
+   !output#load !last_uri ;
+   ignore(!output#connect#jump jump_callback) ;
+   ignore(!output#connect#selection_changed selection_changed_callback) ;
+;;
+
+let set_anti_aliasing output button_set_anti_aliasing () =
+ !output#set_anti_aliasing button_set_anti_aliasing#active
+;;
+
+let set_kerning output button_set_kerning () =
+ !output#set_kerning button_set_kerning#active
 ;;
 
 let changefont output font_size_spinb () =
@@ -459,47 +478,70 @@ let set_log_verbosity output log_verbosity_spinb () =
  !output#set_log_verbosity log_verbosity_spinb#value_as_int
 ;;
 
-class settings_window output sw jump_callback selection_changed_callback
- last_uri
+class settings_window output sw button_export_to_postscript jump_callback
+ selection_changed_callback last_uri
 =
  let settings_window = GWindow.window ~title:"GtkMathView settings" () in
- let table = GPack.table ~rows:5 ~columns:5 ~packing:settings_window#add () in
+ let vbox =
+  GPack.vbox ~packing:settings_window#add () in
+ let table =
+  GPack.table
+   ~rows:1 ~columns:3 ~homogeneous:false ~row_spacings:5 ~col_spacings:5
+   ~border_width:5 ~packing:vbox#(pack () in
  let button_t1 =
   GButton.toggle_button ~label:"activate t1 fonts"
    ~packing:(table#attach ~left:0 ~top:0) () in
+ let button_set_anti_aliasing =
+  GButton.toggle_button ~label:"set_anti_aliasing"
+   ~packing:(table#attach ~left:1 ~top:0) () in
+ let button_set_kerning =
+  GButton.toggle_button ~label:"set_kerning"
+   ~packing:(table#attach ~left:2 ~top:0) () in
+ let table =
+  GPack.table
+   ~rows:2 ~columns:2 ~homogeneous:false ~row_spacings:5 ~col_spacings:5
+   ~border_width:5 ~packing:vbox#add () in
+ let font_size_label =
+  GMisc.label ~text:"font size:"
+   ~packing:(table#attach ~left:0 ~top:0 ~expand:`NONE) () in
  let font_size_spinb =
   let sadj =
    GData.adjustment ~value:14.0 ~lower:5.0 ~upper:50.0 ~step_incr:1.0 ()
   in
    GEdit.spin_button 
-    ~adjustment:sadj ~packing:(table#attach ~left:4 ~top:2) () in
- let button_set_anti_aliasing = GButton.toggle_button ~label:"set_anti_aliasing" ~packing:(table#attach ~left:1 ~top:3) () in
- let button_set_kerning =
-  GButton.toggle_button ~label:"set_kerning"
-   ~packing:(table#attach ~left:3 ~top:3) () in
+    ~adjustment:sadj ~packing:(table#attach ~left:1 ~top:0 ~fill:`NONE) () in
+ let log_verbosity_label =
+  GMisc.label ~text:"log verbosity:"
+   ~packing:(table#attach ~left:0 ~top:1) () in
  let log_verbosity_spinb =
   let sadj =
    GData.adjustment ~value:0.0 ~lower:0.0 ~upper:3.0 ~step_incr:1.0 ()
   in
    GEdit.spin_button 
-    ~adjustment:sadj ~packing:(table#attach ~left:2 ~top:2) () in
+    ~adjustment:sadj ~packing:(table#attach ~left:1 ~top:1) () in
+ let hbox =
+  GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
+ let closeb =
+  GButton.button ~label:"Close"
+   ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
 object(self)
  method show = settings_window#show
  initializer
+  button_set_anti_aliasing#misc#set_sensitive false ;
+  button_set_kerning#misc#set_sensitive false ;
   (* Signals connection *)
-  let is_set_use_t1_lib = ref false in
-   ignore(button_t1#connect#clicked
-    (activate_t1 output sw is_set_use_t1_lib jump_callback
-     selection_changed_callback last_uri)) ;
+  ignore(button_t1#connect#clicked
+   (activate_t1 output button_set_anti_aliasing button_set_kerning
+    button_export_to_postscript sw button_t1 jump_callback
+    selection_changed_callback last_uri)) ;
   ignore(font_size_spinb#connect#changed (changefont output font_size_spinb)) ;
-  let is_set_anti_aliasing = ref false in
-   ignore(button_set_anti_aliasing#connect#toggled
-    (set_anti_aliasing output is_set_anti_aliasing));
-  let is_set_kerning = ref false in
-   ignore(button_set_kerning#connect#toggled
-    (set_kerning output is_set_kerning)) ;
+  ignore(button_set_anti_aliasing#connect#toggled
+   (set_anti_aliasing output button_set_anti_aliasing));
+  ignore(button_set_kerning#connect#toggled
+   (set_kerning output button_set_kerning)) ;
   ignore(log_verbosity_spinb#connect#changed
-   (set_log_verbosity output log_verbosity_spinb))
+   (set_log_verbosity output log_verbosity_spinb)) ;
+  ignore(closeb#connect#clicked settings_window#misc#hide)
 end;;
 
 (* Main windows *)
@@ -629,6 +671,7 @@ object(self)
  initializer
   nextb#misc#set_sensitive false ;
   prevb#misc#set_sensitive false ;
+  button_export_to_postscript#misc#set_sensitive false ;
 
   (* signal handlers here *)
   ignore(!output#connect#jump (jump self)) ;
@@ -639,7 +682,7 @@ object(self)
   ignore(closeb#connect#clicked window#misc#hide) ;
   ignore(annotateb#connect#clicked (annotateb_pressed self annotation_window)) ;
   let settings_window = new settings_window output scrolled_window0
-   (jump self) (choose_selection self) loaded_uri in
+   button_export_to_postscript (jump self) (choose_selection self) loaded_uri in
   ignore(settingsb#connect#clicked settings_window#show) ;
   ignore(button_export_to_postscript#connect#clicked (export_to_postscript output)) ;
   ignore(window#event#connect#delete (fun _ -> window#misc#hide () ; true ))
@@ -694,6 +737,7 @@ object(self)
  initializer
   nextb#misc#set_sensitive false ;
   prevb#misc#set_sensitive false ;
+  button_export_to_postscript#misc#set_sensitive false ;
 
   (* signal handlers here *)
   ignore(!output#connect#jump (jump rendering_window)) ;
@@ -702,7 +746,8 @@ object(self)
   ignore(prevb#connect#clicked (theory_prev self)) ;
   ignore(checkb#connect#clicked (theory_check self)) ;
   let settings_window = new settings_window output scrolled_window0
-   (jump rendering_window) (choose_selection self) theory_loaded_uri in
+   button_export_to_postscript (jump rendering_window) (choose_selection self)
+   theory_loaded_uri in
   ignore(settingsb#connect#clicked settings_window#show) ;
   ignore(button_export_to_postscript#connect#clicked (export_to_postscript output)) ;
   ignore(closeb#connect#clicked window#misc#hide) ;