diff options
Diffstat (limited to 'ide')
-rw-r--r-- | ide/coqide.ml | 2 | ||||
-rw-r--r-- | ide/session.ml | 4 | ||||
-rw-r--r-- | ide/wg_MessageView.ml | 10 | ||||
-rw-r--r-- | ide/wg_MessageView.mli | 1 |
4 files changed, 11 insertions, 6 deletions
diff --git a/ide/coqide.ml b/ide/coqide.ml index 8a64e5184..8429a9b07 100644 --- a/ide/coqide.ml +++ b/ide/coqide.ml @@ -748,7 +748,7 @@ let refresh_editor_prefs () = (* Fonts *) sn.script#misc#modify_font fd; sn.proof#misc#modify_font fd; - sn.messages#misc#modify_font fd; + sn.messages#modify_font fd; sn.command#refresh_font (); (* Colors *) diff --git a/ide/session.ml b/ide/session.ml index 6342f698b..8eeb3c6f9 100644 --- a/ide/session.ml +++ b/ide/session.ml @@ -198,8 +198,6 @@ let build_layout (sn:session) = ~vpolicy:`AUTOMATIC ~hpolicy:`AUTOMATIC ~packing:proof_frame#add () in let message_frame = GBin.frame ~shadow_type:`IN ~packing:state_paned#add2 () in - let message_scroll = GBin.scrolled_window - ~vpolicy:`AUTOMATIC ~hpolicy:`AUTOMATIC ~packing:message_frame#add () in let session_tab = GPack.hbox ~homogeneous:false () in let img = GMisc.image ~icon_size:`SMALL_TOOLBAR ~packing:session_tab#pack () in @@ -229,7 +227,7 @@ let build_layout (sn:session) = session_paned#pack2 ~shrink:false ~resize:false (sn.command#frame#coerce); script_scroll#add sn.script#coerce; proof_scroll#add sn.proof#coerce; - message_scroll#add sn.messages#coerce; + message_frame#add sn.messages#coerce; session_tab#pack sn.tab_label#coerce; img#set_stock `YES; eval_paned#set_position 1; diff --git a/ide/wg_MessageView.ml b/ide/wg_MessageView.ml index b57f55ea9..d3513536e 100644 --- a/ide/wg_MessageView.ml +++ b/ide/wg_MessageView.ml @@ -16,18 +16,22 @@ class type message_view = (** same as [add], but with an explicit level instead of [Notice] *) method buffer : GText.buffer (** for more advanced text edition *) + method modify_font : Pango.font_description -> unit end let message_view () : message_view = let buffer = GText.buffer ~tag_table:Tags.Message.table () in - let view = GText.view ~buffer + let box = GPack.vbox () in + let scroll = GBin.scrolled_window + ~vpolicy:`AUTOMATIC ~hpolicy:`AUTOMATIC ~packing:(box#pack ~expand:true) () in + let view = GText.view ~buffer ~packing:scroll#add ~editable:false ~cursor_visible:false ~wrap_mode:`WORD () in let default_clipboard = GData.clipboard Gdk.Atom.primary in let _ = buffer#add_selection_clipboard default_clipboard in let () = view#set_left_margin 2 in object (self) - inherit GObj.widget view#as_widget + inherit GObj.widget box#as_widget method clear = buffer#set_text "" @@ -47,4 +51,6 @@ let message_view () : message_view = method buffer = buffer + method modify_font fd = view#misc#modify_font fd + end diff --git a/ide/wg_MessageView.mli b/ide/wg_MessageView.mli index 215521cda..cb84ae733 100644 --- a/ide/wg_MessageView.mli +++ b/ide/wg_MessageView.mli @@ -16,6 +16,7 @@ class type message_view = (** same as [add], but with an explicit level instead of [Notice] *) method buffer : GText.buffer (** for more advanced text edition *) + method modify_font : Pango.font_description -> unit end val message_view : unit -> message_view |