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, 7 insertions, 0 deletions

diff --git a/plugins/extraction/common.ml b/plugins/extraction/common.ml
index 61e2f8c28f..ad2f400632 100644
--- a/plugins/extraction/common.ml
+++ b/plugins/extraction/common.ml
@@ -41,6 +41,13 @@ let pr_binding = function
   | [] -> mt ()
   | l  -> str " " ++ prlist_with_sep (fun () -> str " ") pr_id l
 
+(** By default, in module Format, you can do horizontal placing of blocks
+    even if they include newlines, as long as the number of chars in the
+    blocks are less that a line length. To avoid this awkward situation,
+    we attach a big virtual size to [fnl] newlines. *)
+
+let fnl () = stras (1000000,"") ++ fnl ()
+
 let fnl2 () = fnl () ++ fnl ()
 
 let space_if = function true -> str " " | false -> mt ()