diff options
| -rw-r--r-- | CHANGES | 3 | ||||
| -rw-r--r-- | lib/pp_control.ml | 6 | ||||
| -rw-r--r-- | lib/pp_control.mli | 3 | ||||
| -rwxr-xr-x | syntax/PPConstr.v | 6 | ||||
| -rw-r--r-- | toplevel/vernacentries.ml | 8 |
5 files changed, 22 insertions, 4 deletions
@@ -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 44f351458..caa985c18 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 256cc26de..b7cc42d11 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 ddc6e3563..9094b0395 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 ed1c52de9..1cf01bf11 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 -> |