- the font size spinner is now initialized with the right value
~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 ()
+ GData.adjustment ~value:(float_of_int output#get_font_size)
+ ~lower:5.0 ~upper:50.0 ~step_incr:1.0 ()
in
GEdit.spin_button
~adjustment:sadj ~packing:(table#attach ~left:1 ~top:0 ~fill:`NONE) () in
inherit GMathViewAux.single_selection_math_view obj
+ initializer self#set_font_size 10
+
val mutable current_infos = None
method make_sequent_of_selected_term =