[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, 7 insertions, 4 deletions

diff --git a/ide/richpp.mli b/ide/richpp.mli
index 980d27407f..0ceeeefc29 100644
--- a/ide/richpp.mli
+++ b/ide/richpp.mli
@@ -16,12 +16,15 @@ type 'annotation located = {
   endpos     : int
 }
 
-(** [rich_pp get_annotations ppcmds] returns the interpretation
+(* XXX: The width parameter should be moved to a `formatter_property`
+   record shared with Topfmt *)
+
+(** [rich_pp width get_annotations ppcmds] returns the interpretation
     of [ppcmds] as a semi-structured document
     that represents (located) annotations of this string.
     The [get_annotations] function is used to convert tags into the desired
-    annotation. *)
-val rich_pp :
+    annotation. [width] sets the printing witdh of the formatter. *)
+val rich_pp : int ->
   (Pp.pp_tag -> 'annotation option) -> Pp.std_ppcmds ->
   'annotation located Xml_datatype.gxml
 
@@ -46,5 +49,5 @@ type richpp = Xml_datatype.xml
 
 (** Type of text with style annotations *)
 
-val richpp_of_pp : Pp.std_ppcmds -> richpp
+val richpp_of_pp : int -> Pp.std_ppcmds -> richpp
 (** Extract style information from formatted text *)