src/gtk/newgui/gui_console_base.ml

   1 class box () =
   2   let _anonymous_container_1 = GPack.vbox ~homogeneous:false () in
   3   let _anonymous_container_2 =
   4     GBin.scrolled_window ~hpolicy:`AUTOMATIC ~vpolicy:`AUTOMATIC
   5       ~placement:`TOP_LEFT
   6       ~packing:(_anonymous_container_1#pack ~expand:true ~fill:true) ()
   7   in
   8   let text =
   9     GEdit.text ~editable:false ~word_wrap:true ~line_wrap:true
  10       ~packing:(_anonymous_container_2#add) ()
  11   in
  12   let _anonymous_container_3 =
  13     GPack.hbox ~homogeneous:false
  14       ~packing:(_anonymous_container_1#pack ~expand:false ~fill:true) ()
  15   in
  16   let _ =
  17     GMisc.label ~width:180 ~text:(Gui_messages.cT_lb_command)
  18       ~justify:`LEFT ~line_wrap:true ~xalign:(-1.0) ~yalign:(-1.0)
  19       ~packing:(_anonymous_container_3#pack ~expand:false ~fill:true) ()
  20   in
  21   let we_command =
  22     GEdit.combo ~popdown_strings:[] ~use_arrows:`DEFAULT ~case_sensitive:true
  23       ~value_in_list:false ~ok_if_empty:true
  24       ~packing:(_anonymous_container_3#pack ~expand:true ~fill:true) ()
  25   in
  26   let wb_clear_console =
  27     GButton.button
  28       ~packing:(_anonymous_container_3#pack ~expand:false ~fill:true) ()
  29   in
  30   let _ =
  31     GMisc.label ~width:180 ~text:(Gui_messages.cT_lb_clear_console)
  32       ~justify:`RIGHT ~line_wrap:true ~xalign:(-1.0) ~yalign:(-1.0)
  33       ~packing:(wb_clear_console#add) ()
  34   in
  35   object
  36     val text = text
  37     val we_command = we_command
  38     val wb_clear_console = wb_clear_console
  39     method text = text
  40     method we_command = we_command
  41     method wb_clear_console = wb_clear_console
  42     method coerce = _anonymous_container_1#coerce
  43   end