Repair Haskell/Scheme extraction in the new extraction backend design:

Unlike prlist_xxxx and prvect, the function prlist is acting lazily,
which is bad for extraction (synchronization with tables).  We add and
use a prlist_strict function.

Additionaly: 
 - cleanup of the preamble printing
 - no need for 2-pass printing (/dev/null trick) when the language 
   isn't ocaml



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

1 files changed, 9 insertions, 13 deletions

diff --git a/contrib/extraction/scheme.ml b/contrib/extraction/scheme.ml
index 5048002d0..b6724f584 100644
--- a/contrib/extraction/scheme.ml
+++ b/contrib/extraction/scheme.ml
@@ -30,16 +30,10 @@ let keywords =
     Idset.empty
 
 let preamble _ _ usf = 
-  str ";; This extracted scheme code relies on some additional macros" ++ 
-  fnl () ++
-  str ";; available at http://www.pps.jussieu.fr/~letouzey/scheme" ++
-  fnl () ++
-  str "(load \"macros_extr.scm\")" ++
-  fnl () ++ fnl () ++
-  (if usf.mldummy then 
-     str "(define __ (lambda (_) __))" 
-     ++ fnl () ++ fnl()
-   else mt ())
+  str ";; This extracted scheme code relies on some additional macros\n" ++ 
+  str ";; available at http://www.pps.jussieu.fr/~letouzey/scheme\n" ++
+  str "(load \"macros_extr.scm\")\n\n" ++
+  (if usf.mldummy then str "(define __ (lambda (_) __))\n\n" else mt ())
 
 let pr_id id = 
   let s = string_of_id id in
@@ -60,7 +54,7 @@ let pp_apply st _ = function
   | [] -> st 
   | [a] -> hov 2 (paren (st ++ spc () ++ a))
   | args -> hov 2 (paren (str "@ " ++ st ++ 
-			  (prlist (fun x -> spc () ++ x) args))) 
+			  (prlist_strict (fun x -> spc () ++ x) args)))
 
 (*s The pretty-printer for Scheme syntax *)
 
@@ -189,9 +183,11 @@ let pp_structure_elem = function
 
 let pp_struct = 
   let pp_sel (mp,sel) = 
-    push_visible mp; let p = prlist pp_structure_elem sel in pop_visible (); p
+    push_visible mp; 
+    let p = prlist_strict pp_structure_elem sel in 
+    pop_visible (); p
   in
-  prlist pp_sel
+  prlist_strict pp_sel
 
 let scheme_descr = {
   keywords = keywords;