Ajout de Set Print Width

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

5 files changed, 22 insertions, 4 deletions

diff --git a/CHANGES b/CHANGES
index a72a1da2e3..6ebd9b2811 100644
--- a/CHANGES
+++ b/CHANGES
@@ -5,7 +5,8 @@ Vernacular commands
 
 - "Declare ML Module" now allows us to import .cma files. This avoids to use a
    bunch of "Declare ML Module" statements when using several ML files.
-
+- "Set Printing Width n" added, allows to change the size of width printing
+   (TODO : doc).
 Gallina
 
 - New syntax of the form "Inductive bool : Set := true, false : bool." for
diff --git a/lib/pp_control.ml b/lib/pp_control.ml
index 44f3514588..caa985c185 100644
--- a/lib/pp_control.ml
+++ b/lib/pp_control.ml
@@ -96,7 +96,13 @@ let _ = set_gp deep_ft deep_gp
 
 (* For parametrization through vernacular *)
 let default = Format.pp_get_max_boxes !std_ft ()
+let default_margin = Format.pp_get_margin !std_ft ()
+
 let get_depth_boxes () = Some (Format.pp_get_max_boxes !std_ft ())
 let set_depth_boxes v =
   Format.pp_set_max_boxes !std_ft (match v with None -> default | Some v -> v)
 
+let get_margin () = Some (Format.pp_get_margin !std_ft ())
+let set_margin v =
+  Format.pp_set_margin !std_ft (match v with None -> default_margin | Some v -> v)
+
diff --git a/lib/pp_control.mli b/lib/pp_control.mli
index 256cc26dea..b7cc42d112 100644
--- a/lib/pp_control.mli
+++ b/lib/pp_control.mli
@@ -44,3 +44,6 @@ val deep_ft : Format.formatter
 
 val set_depth_boxes : int option -> unit
 val get_depth_boxes : unit -> int option
+
+val set_margin : int option -> unit
+val get_margin : unit -> int option
diff --git a/syntax/PPConstr.v b/syntax/PPConstr.v
index ddc6e35638..9094b0395c 100755
--- a/syntax/PPConstr.v
+++ b/syntax/PPConstr.v
@@ -34,7 +34,7 @@ Syntax constr
        [ [<hov 0> (IDBINDER ($LIST $id))] ":" $c:E ]
 
   | letbinder  [ << (BINDERS (LETBINDER $c $id)) >> ] -> 
-       [ [<hov 0> $id ":=" $c:E ] ]
+       [ [<hov 0> id ":=" [0 1] $c:E ] ]
   ;
 
 
@@ -146,8 +146,8 @@ Syntax constr
 (* redundant
   | let [ [$x = $M]$N ] -> [ [<hov 0> "[" $x "=" $M:E "]" [0 1] $N:E ] ]
 *)
-  | letin [ << (LETIN $A [$x]$B) >> ] -> [ [ <hov 0> "[" $x ":=" $A:E "]" [0 1] $B:E ] ]
-  | letincast [ << (LETIN (CAST $A $C) [$x]$B) >> ] -> [ [ <hov 0> "[" $x ":=" $A:E ":" $C:E "]" [0 1] $B:E ] ]
+  | letin [ << (LETIN $A [$x]$B) >> ] -> [ [ <hov 0> "[" $x ":=" [0 1] $A:E "]" [0 1] $B:E ] ]
+  | letincast [ << (LETIN (CAST $A $C) [$x]$B) >> ] -> [ [ <hov 0> "[" $x ":=" [0 1] $A:E ":" $C:E "]" [0 1] $B:E ] ]
   ;
 
 (* Things parsed in command9 *)
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index ed1c52de91..1cf01bf11b 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -791,6 +791,14 @@ let _ =
       optread=Pp_control.get_depth_boxes;
       optwrite=Pp_control.set_depth_boxes }
 
+let _ =
+  declare_int_option
+    { optsync=true;
+      optkey=SecondaryTable("Printing","Width");
+      optname="the printing width";
+      optread=Pp_control.get_margin;
+      optwrite=Pp_control.set_margin}
+
 let vernac_set_opacity opaq locqid =
   match Nametab.global locqid with
     | ConstRef sp ->