Extraction: improved indentation of extracted code (fix #2497)

 For Haskell, we still try to provide readable indentation,
 but we now avoid relying on this indentation for correctness.
 Instead, we use layout-independant syntax with { } when
 necessary (after "case of" and "let"). It is much safer this
 way, even if the syntax gets a bit more cumbersome.

 For people allergic to {;}, they can most of the time do a
 tr -d "{;}" without changing the meaning of the program.
 Be careful nonetheless: since "case of" is now delimited,
 some parenthesis that used to be mandatory are now removed.

 Note also that the initial "module ... where" is still without
 { }: even when Format goes crazy it doesn't tamper with column 0.

 Other modifications:

 - Using "Set Printing Width" now affects uniformly the extraction
 pretty-printers. You can set a greater value than the default 78
 before extracting a program that you know to be "really deep".

 - In ocaml (and also a bit in Haskell), we now try to avoid abusing
 of 2-char-right-indentation. For instance | is now aligned with
 the "m" of match. This way, max_indent will be reached less frequently.

 - As soon as a pretty-print box contains an explicit newline,
 we set its virtual size to a big number, in order to prevent this
 box to be part of some horizontal arrangement.

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

1 files changed, 14 insertions, 7 deletions

diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml
index 1218dd80c5..8a812664ff 100644
--- a/plugins/extraction/extract_env.ml
+++ b/plugins/extraction/extract_env.ml
@@ -395,13 +395,20 @@ let print_one_decl struc mp decl =
 (*s Extraction of a ml struct to a file. *)
 
 let formatter dry file =
-  if dry then Format.make_formatter (fun _ _ _ -> ()) (fun _ -> ())
-  else match file with
-    | None -> !Pp_control.std_ft
-    | Some cout ->
-	let ft = Pp_control.with_output_to cout in
-	Option.iter (Format.pp_set_margin ft) (Pp_control.get_margin ());
-	ft
+  let ft =
+    if dry then Format.make_formatter (fun _ _ _ -> ()) (fun _ -> ())
+    else Pp_control.with_output_to (Option.default stdout file)
+  in
+  (* We never want to see ellipsis ... in extracted code *)
+  Format.pp_set_max_boxes ft max_int;
+  (* We reuse the width information given via "Set Printing Width" *)
+  (match Pp_control.get_margin () with
+    | None -> ()
+    | Some i ->
+      Format.pp_set_margin ft i;
+      Format.pp_set_max_indent ft (i-10));
+      (* note: max_indent should be < margin above, otherwise it's ignored *)
+  ft
 
 let print_structure_to_file (fn,si,mo) dry struc =
   let d = descr () in