From 8b1bd5bb6bb66a578969e0a4f8c535a3718bba8c Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Mon, 10 Feb 2020 16:06:50 +0100
Subject: Another micro-improvement in printing "fix".

Set Printing Width 20.
Check fix my_long_fix
 (my_induction_variable y z t u v w x' y' z' t' u' v' w' : nat)
 (a b c d e f a' b' c' d' e' f' : bool) :=
 match my_induction_variable with
 | 0 => 0
 | S my_recursive_variable => my_recursive_variable
 end.

gives:

fix my_long_fix
  (my_induction_variable
   y z t u v w x'
   y' z' t' u' v'
   w' : nat)
  (a b c d e f a'
   b' c' d' e'
   f' : bool)
  {struct
   my_induction_variable} :
    nat :=
  match
    my_induction_variable
  with
  | 0 => 0
  | S
    my_recursive_variable =>
      my_recursive_variable
  end

instead of:

fix
my_long_fix (my_induction_variable
            y z t u
            v w x'
            y' z'
            t' u'
            v'
            w' : nat)
            (a b c
            d e f
            a' b'
            c' d'
            e'
            f' : bool)
            {struct
            my_induction_variable} :
  nat :=
  match
    my_induction_variable
  with
  | 0 => 0
  | S
    my_recursive_variable =>
      my_recursive_variable
  end
---
 printing/ppconstr.ml | 12 ++++++------
 1 file changed, 6 insertions(+), 6 deletions(-)

diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml
index 49c475dff4..814b1b0a06 100644
--- a/printing/ppconstr.ml
+++ b/printing/ppconstr.ml
@@ -223,7 +223,7 @@ let tag_var = tag Tag.variable
 
   let pr_opt_type_spc pr = function
     | { CAst.v = CHole (_,IntroAnonymous,_) } -> mt ()
-    | t ->  str " :" ++ pr_sep_com (fun()->brk(1,2)) (pr ltop) t
+    | t ->  str " :" ++ pr_sep_com (fun()->brk(1,4)) (pr ltop) t
 
   let pr_prim_token = function
     | Numeral (SPlus,n) -> str (NumTok.to_string n)
@@ -387,7 +387,7 @@ let tag_var = tag Tag.variable
   let pr_recursive_decl pr pr_dangling kw dangling_with_for id bl annot t c =
     let pr_body =
       if dangling_with_for then pr_dangling else pr in
-    hov 0 (str kw ++ spc () ++ pr_id id ++ (if bl = [] then mt () else str" ") ++
+    hov 0 (str kw ++ brk(1,2) ++ pr_id id ++ (if bl = [] then mt () else brk(1,2)) ++
       hov 0 (pr_undelimited_binders spc (pr ltop) bl ++ annot) ++
       pr_opt_type_spc pr t ++ str " :=") ++
       pr_sep_com (fun () -> brk(1,2)) (pr_body ltop) c
@@ -404,13 +404,13 @@ let tag_var = tag Tag.variable
               | CLocalPattern _ -> assert false
             in let ids = List.flatten (List.map names_of_binder bl) in
                if List.length ids > 1 then
-                 spc() ++ str "{" ++ keyword "struct" ++ spc () ++ pr_id id ++ str"}"
+                 spc() ++ str "{" ++ keyword "struct" ++ brk (1,1) ++ pr_id id ++ str"}"
                else mt()
           | CWfRec (id,c) ->
-            spc() ++ str "{" ++ keyword "wf" ++ spc () ++ pr_aux c ++ spc() ++ pr_lident id ++ str"}"
+            spc() ++ str "{" ++ keyword "wf" ++ brk (1,1) ++ pr_aux c ++ brk (1,1) ++ pr_lident id ++ str"}"
           | CMeasureRec (id,m,r) ->
-            spc() ++ str "{" ++ keyword "measure" ++ spc () ++ pr_aux m ++
-            match id with None -> mt() | Some id -> spc () ++ pr_lident id ++
+            spc() ++ str "{" ++ keyword "measure" ++ brk (1,1) ++ pr_aux m ++
+            match id with None -> mt() | Some id -> brk (1,1) ++ pr_lident id ++
               (match r with None -> mt() | Some r -> str" on " ++ pr_aux r) ++ str"}"
 
   let pr_fixdecl pr prd kw dangling_with_for ({v=id},ro,bl,t,c) =
-- 
cgit v1.2.3