Now CoqIDE auto-sets the printing width of the goal display.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15494 85f007b7-540e-0410-9357-904b9bb8a0f7

5 files changed, 18 insertions, 0 deletions

diff --git a/ide/coq.ml b/ide/coq.ml
index dd0959726..31de9cf4b 100644
--- a/ide/coq.ml
+++ b/ide/coq.ml
@@ -427,6 +427,11 @@ let reset_coqtop coqtop hook =
 module PrintOpt =
 struct
   type t = string list
+
+  let width_ref = ref None
+  let set_printing_width w = width_ref := Some w
+
+  let width = ["Printing"; "Width"]
   let implicit = ["Printing"; "Implicit"]
   let coercions = ["Printing"; "Coercions"]
   let raw_matching = ["Printing"; "Matching"; "Synth"]
@@ -442,6 +447,7 @@ struct
   let set coqtop options =
     let () = List.iter (fun (name, v) -> Hashtbl.replace state_hack name v) options in
     let options = List.map (fun (name, v) -> (name, Interface.BoolValue v)) options in
+    let options = (width, Interface.IntValue !width_ref):: options in
     match eval_call coqtop (Serialize.set_options options) with
     | Interface.Good () -> ()
     | _ -> raise (Failure "Cannot set options.")
diff --git a/ide/coq.mli b/ide/coq.mli
index a0f192c01..f168aff80 100644
--- a/ide/coq.mli
+++ b/ide/coq.mli
@@ -112,5 +112,6 @@ sig
   val existential : t
   val universes : t
 
+  val set_printing_width : int -> unit
   val set : handle -> (t * bool) list -> unit
 end
diff --git a/ide/coqide.ml b/ide/coqide.ml
index 85c341b4c..a1e910b40 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -624,6 +624,7 @@ object(self)
       if current.contextual_menus_on_goal then
         ignore (self#insert_this_phrase_on_success handle ("progress "^s) s)
     in
+    Coq.PrintOpt.set_printing_width (textview_width proof_view);
     match Coq.goals handle with
     | Interface.Fail (l, str) ->
       self#set_message ("Error in coqtop:\n"^str)
diff --git a/ide/ideutils.ml b/ide/ideutils.ml
index ddf95e25e..2a5df0ea9 100644
--- a/ide/ideutils.ml
+++ b/ide/ideutils.ml
@@ -325,3 +325,10 @@ let url_for_keyword =
 let browse_keyword f text =
   try let u = Lazy.force url_for_keyword text in browse f (doc_url() ^ u)
   with Not_found -> f ("No documentation found for \""^text^"\".\n")
+
+let textview_width (view : #GText.view) =
+  let rect = view#visible_rect in
+  let pixel_width = Gdk.Rectangle.width rect in
+  let metrics = view#misc#pango_context#get_metrics ()  in
+  let char_width = GPango.to_pixels metrics#approx_char_width in
+  pixel_width / char_width
diff --git a/ide/ideutils.mli b/ide/ideutils.mli
index 5aa615549..553c4c2bc 100644
--- a/ide/ideutils.mli
+++ b/ide/ideutils.mli
@@ -67,3 +67,6 @@ val pbar : GRange.progress_bar
    everything. Reference: http://ss64.com/nt/cmd.html *)
 
 val requote : string -> string
+
+val textview_width : #GText.view -> int
+(** Returns an approximate value of the character width of a textview *)