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

diff --git a/plugins/extraction/common.mli b/plugins/extraction/common.mli
index 0abb47c229..7fc3279afc 100644
--- a/plugins/extraction/common.mli
+++ b/plugins/extraction/common.mli
@@ -12,6 +12,12 @@ open Miniml
 open Mlutil
 open Pp
 
+(** 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. *)
+
+val fnl : unit -> std_ppcmds
 val fnl2 : unit -> std_ppcmds
 val space_if : bool -> std_ppcmds