src/gtk/newgui/gui_help_base.ml

   1 class box () =
   2   let wscroll =
   3     GBin.scrolled_window ~hpolicy:`AUTOMATIC ~vpolicy:`AUTOMATIC
   4       ~placement:`TOP_LEFT ()
   5   in
   6   let wtext =
   7     GEdit.text ~editable:false ~word_wrap:true ~line_wrap:true
   8       ~packing:(wscroll#add) ()
   9   in
  10   object
  11     val wscroll = wscroll
  12     val wtext = wtext
  13     method wscroll = wscroll
  14     method wtext = wtext
  15     method coerce = wscroll#coerce
  16   end