diff options
Diffstat (limited to 'ide/wg_MessageView.ml')
| -rw-r--r-- | ide/wg_MessageView.ml | 96 |
1 files changed, 64 insertions, 32 deletions
diff --git a/ide/wg_MessageView.ml b/ide/wg_MessageView.ml index 0330b8ef..a79a093e 100644 --- a/ide/wg_MessageView.ml +++ b/ide/wg_MessageView.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Preferences @@ -28,13 +30,14 @@ class type message_view = inherit GObj.widget method connect : message_view_signals method clear : unit - method add : Richpp.richpp -> unit + method add : Pp.t -> unit method add_string : string -> unit - method set : Richpp.richpp -> unit + method set : Pp.t -> unit + method refresh : bool -> unit method push : Ideutils.logger (** same as [add], but with an explicit level instead of [Notice] *) - method buffer : GText.buffer - (** for more advanced text edition *) + method has_selection : bool + method get_selected_text : string end let message_view () : message_view = @@ -42,7 +45,6 @@ let message_view () : message_view = ~highlight_matching_brackets:true ~tag_table:Tags.Message.table () in - let text_buffer = new GText.buffer buffer#as_buffer in let mark = buffer#create_mark ~left_gravity:false buffer#start_iter in let box = GPack.vbox () in let scroll = GBin.scrolled_window @@ -57,46 +59,76 @@ let message_view () : message_view = let () = view#set_left_margin 2 in view#misc#show (); let cb clr = view#misc#modify_base [`NORMAL, `NAME clr] in - let _ = background_color#connect#changed cb in - let _ = view#misc#connect#realize (fun () -> cb background_color#get) in + let _ = background_color#connect#changed ~callback:cb in + let _ = view#misc#connect#realize ~callback:(fun () -> cb background_color#get) in let cb ft = view#misc#modify_font (Pango.Font.from_string ft) in stick text_font view cb; - object (self) + + (* Inserts at point, advances the mark *) + let insert_msg (level, msg) = + let tags = match level with + | Feedback.Error -> [Tags.Message.error] + | Feedback.Warning -> [Tags.Message.warning] + | _ -> [] + in + let mark = `MARK mark in + let width = Ideutils.textview_width view in + Ideutils.insert_xml ~mark buffer ~tags (Richpp.richpp_of_pp width msg); + buffer#insert ~iter:(buffer#get_iter_at_mark mark) "\n" + in + + let mv = object (self) inherit GObj.widget box#as_widget + (* List of displayed messages *) + val mutable last_width = -1 + val mutable msgs = [] + val push = new GUtil.signal () method connect = new message_view_signals_impl box#as_widget push + method refresh force = + (* We need to block updates here due to the following race: + insertion of messages may create a vertical scrollbar, this + will trigger a width change, calling refresh again and + going into an infinite loop. *) + let width = Ideutils.textview_width view in + (* Could still this method race if the scrollbar changes the + textview_width ?? *) + let needed = force || last_width <> width in + if needed then begin + last_width <- width; + buffer#set_text ""; + buffer#move_mark (`MARK mark) ~where:buffer#start_iter; + List.(iter insert_msg (rev msgs)) + end + method clear = - buffer#set_text ""; - buffer#move_mark (`MARK mark) ~where:buffer#start_iter + msgs <- []; self#refresh true method push level msg = - let tags = match level with - | Feedback.Error -> [Tags.Message.error] - | Feedback.Warning -> [Tags.Message.warning] - | _ -> [] - in - let rec non_empty = function - | Xml_datatype.PCData "" -> false - | Xml_datatype.PCData _ -> true - | Xml_datatype.Element (_, _, children) -> List.exists non_empty children - in - if non_empty (Richpp.repr msg) then begin - let mark = `MARK mark in - Ideutils.insert_xml ~mark buffer ~tags msg; - buffer#insert ~iter:(buffer#get_iter_at_mark mark) "\n"; - push#call (level, msg) - end + msgs <- (level, msg) :: msgs; + insert_msg (level, msg); + push#call (level, msg) method add msg = self#push Feedback.Notice msg - method add_string s = self#add (Richpp.richpp_of_string s) + method add_string s = self#add (Pp.str s) method set msg = self#clear; self#add msg - method buffer = text_buffer + method has_selection = buffer#has_selection + method get_selected_text = + if buffer#has_selection then + let start, stop = buffer#selection_bounds in + buffer#get_text ~slice:true ~start ~stop () + else "" end + in + (* Is there a better way to connect the signal ? *) + let w_cb (_ : Gtk.rectangle) = mv#refresh false in + ignore (view#misc#connect#size_allocate ~callback:w_cb); + mv |