[ide] Dynamic printing width.

The IDE now gets core Coq's `std_ppcmds` document format which is
width-independent.

Thus, we follow [1] and make the `{proof,message}_view` object refresh
their contents when the container widget changes size (by listening to
GTK's `size_allocated` signal). The practical advantage is that now
CoqIDE always renders terms with the proper printing width set and
without a roundtrip to Coq.

This patch dispenses the need for the `printing width` option, which
could be removed altogether.

[1] http://stackoverflow.com/questions/40854571/change-gtksourceview-contents-on-resize/

1 files changed, 46 insertions, 13 deletions

diff --git a/ide/wg_MessageView.ml b/ide/wg_MessageView.ml
index 1cf389c75..3d0cd46cd 100644
--- a/ide/wg_MessageView.ml
+++ b/ide/wg_MessageView.ml
@@ -31,6 +31,7 @@ class type message_view =
     method add : Pp.std_ppcmds -> unit
     method add_string : string -> unit
     method set : Pp.std_ppcmds -> unit
+    method refresh : bool -> unit
     method push : Ideutils.logger
       (** same as [add], but with an explicit level instead of [Notice] *)
     method buffer : GText.buffer
@@ -57,31 +58,58 @@ 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 mark = `MARK mark in
-      Ideutils.insert_xml ~mark buffer ~tags (Richpp.richpp_of_pp msg);
-      buffer#insert ~iter:(buffer#get_iter_at_mark mark) "\n";
+      msgs <- (level, msg) :: msgs;
+      insert_msg (level, msg);
       push#call (level, msg)
 
     method add msg = self#push Feedback.Notice msg
@@ -93,3 +121,8 @@ let message_view () : message_view =
     method buffer = text_buffer
 
   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