[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/

11 files changed, 82 insertions, 51 deletions

diff --git a/ide/coq.ml b/ide/coq.ml
index e2036beee..bb9d6e522 100644
--- a/ide/coq.ml
+++ b/ide/coq.ml
@@ -549,18 +549,11 @@ struct
 
   let _ = reset ()
 
-  (** Integer option *)
-
-  let width = ["Printing"; "Width"]
-  let width_state = ref None
-  let set_printing_width w = width_state := Some w
-
   (** Transmitting options to coqtop *)
 
   let enforce h k =
     let mkopt o v acc = (o, Interface.BoolValue v) :: acc in
     let opts = Hashtbl.fold mkopt current_state [] in
-    let opts = (width, Interface.IntValue !width_state) :: opts in
     eval_call (Xmlprotocol.set_options opts) h
       (function
 	| Interface.Good () -> k ()
diff --git a/ide/coq.mli b/ide/coq.mli
index f2876de24..ab8c12a6f 100644
--- a/ide/coq.mli
+++ b/ide/coq.mli
@@ -139,7 +139,6 @@ sig
   val bool_items : bool_descr list
 
   val set : t -> bool -> unit
-  val set_printing_width : int -> unit
 
   (** [enforce] transmits to coq the current option values.
       It is also called by [goals] and [evars] above. *)
diff --git a/ide/coqOps.ml b/ide/coqOps.ml
index 7982ffc8b..cee243f91 100644
--- a/ide/coqOps.ml
+++ b/ide/coqOps.ml
@@ -340,7 +340,6 @@ object(self)
     buffer#get_iter_at_mark `INSERT
 
   method private show_goals_aux ?(move_insert=false) () =
-    Coq.PrintOpt.set_printing_width proof#width;
     if move_insert then begin
       let dest = self#get_start_of_input in
       if (buffer#get_iter_at_mark `INSERT)#compare dest <= 0 then begin
diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml
index c77232ad1..e3e1a8890 100644
--- a/ide/ide_slave.ml
+++ b/ide/ide_slave.ml
@@ -112,7 +112,7 @@ let annotate phrase =
     Vernac.parse_sentence (pa,None)
   in
   (* XXX: Width should be a parameter of annotate... *)
-  Richpp.richpp_of_pp (Ppvernac.pr_vernac ast)
+  Richpp.richpp_of_pp 78 (Ppvernac.pr_vernac ast)
 
 (** Goal display *)
 
diff --git a/ide/richpp.ml b/ide/richpp.ml
index b84c51824..515090f71 100644
--- a/ide/richpp.ml
+++ b/ide/richpp.ml
@@ -38,7 +38,7 @@ type 'a context = {
     marking functions. As those functions are called when actually writing to
     the device, the resulting tree is correct.
 *)
-let rich_pp annotate ppcmds =
+let rich_pp width annotate ppcmds =
 
   let context = {
     stack = Leaf;
@@ -113,12 +113,12 @@ let rich_pp annotate ppcmds =
   pp_set_formatter_tag_functions ft tag_functions;
   pp_set_mark_tags ft true;
 
-  (* Set formatter width. This is currently a hack and duplicate code
-     with Pp_control. Hopefully it will be fixed better in Coq 8.7 *)
-  let w = pp_get_margin str_formatter () in
-  let m = max (64 * w / 100) (w-30) in
-  pp_set_margin ft w;
+  (* Setting the formatter *)
+  pp_set_margin ft width;
+  let m = max (64 * width / 100) (width-30) in
   pp_set_max_indent ft m;
+  pp_set_max_boxes ft 50 ;
+  pp_set_ellipsis_text ft "...";
 
   (** The whole output must be a valid document. To that
       end, we nest the document inside <pp> tags. *)
@@ -172,7 +172,7 @@ let xml_of_rich_pp tag_of_annotation attributes_of_annotation xml =
 
 type richpp = xml
 
-let richpp_of_pp pp =
+let richpp_of_pp width pp =
   let annotate t = Some (Ppstyle.repr t)    in
   let rec drop = function
   | PCData s -> [PCData s]
@@ -182,5 +182,5 @@ let richpp_of_pp pp =
     | None -> cs
     | Some s -> [Element (String.concat "." s, [], cs)]
   in
-  let xml = rich_pp annotate pp in
+  let xml = rich_pp width annotate pp in
   Element ("_", [], drop xml)
diff --git a/ide/richpp.mli b/ide/richpp.mli
index 980d27407..0ceeeefc2 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 *)
diff --git a/ide/wg_Command.ml b/ide/wg_Command.ml
index b83bd107e..47dad8f19 100644
--- a/ide/wg_Command.ml
+++ b/ide/wg_Command.ml
@@ -103,11 +103,12 @@ object(self)
       let process =
 	Coq.bind (Coq.query (phrase,Stateid.dummy)) (function
           | Interface.Fail (_,l,str) ->
-            Ideutils.insert_xml result#buffer (Richpp.richpp_of_pp str);
+            let width = Ideutils.textview_width result in
+            Ideutils.insert_xml result#buffer (Richpp.richpp_of_pp width str);
             notebook#set_page ~tab_label:(new_tab_lbl "Error") frame#coerce;
 	    Coq.return ()
           | Interface.Good res ->
-            result#buffer#insert res; 
+            result#buffer#insert res;
             notebook#set_page ~tab_label:(new_tab_lbl arg) frame#coerce;
 	    Coq.return ())
       in
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
diff --git a/ide/wg_MessageView.mli b/ide/wg_MessageView.mli
index a71d345a5..d065fcbc8 100644
--- a/ide/wg_MessageView.mli
+++ b/ide/wg_MessageView.mli
@@ -21,6 +21,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
diff --git a/ide/wg_ProofView.ml b/ide/wg_ProofView.ml
index 72aa9051a..b5405570c 100644
--- a/ide/wg_ProofView.ml
+++ b/ide/wg_ProofView.ml
@@ -18,7 +18,6 @@ class type proof_view =
     method clear : unit -> unit
     method set_goals : Interface.goals option -> unit
     method set_evars : Interface.evar list option -> unit
-    method width : int
   end
 
 (* tag is the tag to be hooked, item is the item covered by this tag, make_menu
@@ -74,6 +73,7 @@ let mode_tactic sel_cb (proof : #GText.view_skel) goals hints = match goals with
       | None -> [], []
       | Some (hl, h) -> (hl, h)
       in
+      let width = Ideutils.textview_width proof in
       let rec insert_hyp hints hs = match hs with
       | [] -> ()
       | hyp :: hs ->
@@ -84,7 +84,7 @@ let mode_tactic sel_cb (proof : #GText.view_skel) goals hints = match goals with
           let () = hook_tag_cb tag hint sel_cb on_hover in
           [tag], hints
         in
-        let () = insert_xml ~tags proof#buffer (Richpp.richpp_of_pp hyp) in
+        let () = insert_xml ~tags proof#buffer (Richpp.richpp_of_pp width hyp) in
         proof#buffer#insert "\n";
         insert_hyp rem_hints hs
       in
@@ -98,13 +98,13 @@ let mode_tactic sel_cb (proof : #GText.view_skel) goals hints = match goals with
           else []
         in
         proof#buffer#insert (goal_str 1 goals_cnt);
-        insert_xml proof#buffer (Richpp.richpp_of_pp cur_goal);
+        insert_xml proof#buffer (Richpp.richpp_of_pp width cur_goal);
         proof#buffer#insert "\n"
       in
       (* Insert remaining goals (no hypotheses) *)
       let fold_goal i _ { Interface.goal_ccl = g } =
         proof#buffer#insert (goal_str i goals_cnt);
-        insert_xml proof#buffer (Richpp.richpp_of_pp g);
+        insert_xml proof#buffer (Richpp.richpp_of_pp width g);
         proof#buffer#insert "\n"
       in
       let () = Util.List.fold_left_i fold_goal 2 () rem_goals in
@@ -122,6 +122,7 @@ let rec flatten = function
 
 let display mode (view : #GText.view_skel) goals hints evars =
   let () = view#buffer#set_text "" in
+  let width = Ideutils.textview_width view in
   match goals with
   | None -> ()
     (* No proof in progress *)
@@ -144,7 +145,7 @@ let display mode (view : #GText.view_skel) goals hints evars =
       (* The proof is finished, with the exception of given up goals. *)
       view#buffer#insert "No more subgoals, but there are some goals you gave up:\n\n";
       let iter goal =
-        insert_xml view#buffer (Richpp.richpp_of_pp goal.Interface.goal_ccl);
+        insert_xml view#buffer (Richpp.richpp_of_pp width goal.Interface.goal_ccl);
         view#buffer#insert "\n"
       in
       List.iter iter given_up_goals;
@@ -153,7 +154,7 @@ let display mode (view : #GText.view_skel) goals hints evars =
       (* All the goals have been resolved but those on the shelf. *)
       view#buffer#insert "All the remaining goals are on the shelf:\n\n";
       let iter goal =
-        insert_xml view#buffer (Richpp.richpp_of_pp goal.Interface.goal_ccl);
+        insert_xml view#buffer (Richpp.richpp_of_pp width goal.Interface.goal_ccl);
         view#buffer#insert "\n"
       in
       List.iter iter shelved_goals
@@ -166,7 +167,7 @@ let display mode (view : #GText.view_skel) goals hints evars =
       view#buffer#insert "This subproof is complete, but there are some unfocused goals:\n\n";
       let iter i goal =
         let () = view#buffer#insert (goal_str (succ i)) in
-        insert_xml view#buffer (Richpp.richpp_of_pp goal.Interface.goal_ccl);
+        insert_xml view#buffer (Richpp.richpp_of_pp width goal.Interface.goal_ccl);
         view#buffer#insert "\n"
       in
       List.iteri iter bg
@@ -192,7 +193,7 @@ let proof_view () =
   let cb ft = view#misc#modify_font (Pango.Font.from_string ft) in
   stick text_font view cb;
 
-  object
+  let pf = object
     inherit GObj.widget view#as_widget
     val mutable goals = None
     val mutable evars = None
@@ -207,9 +208,11 @@ let proof_view () =
 
     method refresh () =
       let dummy _ () = () in
-      display (mode_tactic dummy) (view :> GText.view_skel) goals None evars
-
-    method width = Ideutils.textview_width (view :> GText.view_skel)
+      display (mode_tactic dummy) view goals None evars
   end
-
-(*     ignore (proof_buffer#add_selection_clipboard cb); *)
+  in
+  (* Is there a better way to connect the signal ? *)
+  (* Can this be done in the object constructor? *)
+  let w_cb _ = pf#refresh () in
+  ignore (view#misc#connect#size_allocate w_cb);
+  pf
diff --git a/ide/wg_ProofView.mli b/ide/wg_ProofView.mli
index b6eae48b3..aa01d955d 100644
--- a/ide/wg_ProofView.mli
+++ b/ide/wg_ProofView.mli
@@ -14,7 +14,6 @@ class type proof_view =
     method clear : unit -> unit
     method set_goals : Interface.goals option -> unit
     method set_evars : Interface.evar list option -> unit
-    method width : int
   end
 
 val proof_view : unit -> proof_view