From: Claudio Sacerdoti Coen Date: Wed, 22 Nov 2000 19:05:22 +0000 (+0000) Subject: Some improvements in the settings window X-Git-Tag: nogzip~149 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=73b8a2b8989ae956eef00d63c2eaaf715428e177;p=helm.git Some improvements in the settings window --- diff --git a/helm/interface/mmlinterface.ml b/helm/interface/mmlinterface.ml index 784c9f4b1..cfccfbb3f 100755 --- 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) ;