Extraction: avoid initial strange empty comments after Arnaud's hack

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

5 files changed, 33 insertions, 15 deletions

diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml
index f49b1f375..0b4047f17 100644
--- a/plugins/extraction/extract_env.ml
+++ b/plugins/extraction/extract_env.ml
@@ -453,6 +453,13 @@ let formatter dry file =
       (* note: max_indent should be < margin above, otherwise it's ignored *)
   ft
 
+let get_comment () =
+  let s = file_comment () in
+  if s = "" then None
+  else
+    let split_comment = Str.split (Str.regexp "[ \t\n]+") s in
+    Some (prlist_with_sep spc str split_comment)
+
 let print_structure_to_file (fn,si,mo) dry struc =
   Buffer.clear buf;
   let d = descr () in
@@ -473,14 +480,11 @@ let print_structure_to_file (fn,si,mo) dry struc =
   (* Print the implementation *)
   let cout = if dry then None else Option.map open_out fn in
   let ft = formatter dry cout in
-  let file_comment =
-    let split_comment = Str.split (Str.regexp "[ \t\n]+") (file_comment ()) in
-    prlist_with_sep spc str split_comment
-  in
+  let comment = get_comment () in
   begin try
     (* The real printing of the implementation *)
     set_phase Impl;
-    pp_with ft (d.preamble mo file_comment opened unsafe_needs);
+    pp_with ft (d.preamble mo comment opened unsafe_needs);
     pp_with ft (d.pp_struct struc);
     Option.iter close_out cout;
   with e ->
@@ -494,7 +498,7 @@ let print_structure_to_file (fn,si,mo) dry struc =
        let ft = formatter false (Some cout) in
        begin try
 	 set_phase Intf;
-	 pp_with ft (d.sig_preamble mo file_comment opened unsafe_needs);
+	 pp_with ft (d.sig_preamble mo comment opened unsafe_needs);
 	 pp_with ft (d.pp_sig (signature_of_structure struc));
 	 close_out cout;
        with e ->
diff --git a/plugins/extraction/haskell.ml b/plugins/extraction/haskell.ml
index 33da06f01..5de13e53c 100644
--- a/plugins/extraction/haskell.ml
+++ b/plugins/extraction/haskell.ml
@@ -44,7 +44,9 @@ let preamble mod_name comment used_modules usf =
      str "{- For Hugs, use the option -F\"cpp -P -traditional\" -}")
   ++ fnl () ++ fnl ()
   ++
-  pp_bracket_comment comment ++ fnl () ++ fnl ()
+  (match comment with
+    | None -> mt ()
+    | Some com -> pp_bracket_comment com ++ fnl () ++ fnl ())
   ++
   str "module " ++ pr_upper_id mod_name ++ str " where" ++ fnl2 () ++
   str "import qualified Prelude" ++ fnl () ++
@@ -358,7 +360,7 @@ let haskell_descr = {
   preamble = preamble;
   pp_struct = pp_struct;
   sig_suffix = None;
-  sig_preamble = (fun _ s _ _ -> (pp_bracket_comment s)++fnl());
+  sig_preamble = (fun _ _ _ _ -> mt ());
   pp_sig = (fun _ -> mt ());
   pp_decl = pp_decl;
 }
diff --git a/plugins/extraction/miniml.mli b/plugins/extraction/miniml.mli
index 261a2c6ee..d170acbb0 100644
--- a/plugins/extraction/miniml.mli
+++ b/plugins/extraction/miniml.mli
@@ -196,13 +196,17 @@ type language_descr = {
   (* Concerning the source file *)
   file_suffix : string;
   (* the second argument is a comment to add to the preamble *)
-  preamble : identifier -> std_ppcmds -> module_path list -> unsafe_needs -> std_ppcmds;
+  preamble :
+    identifier -> std_ppcmds option -> module_path list -> unsafe_needs ->
+    std_ppcmds;
   pp_struct : ml_structure -> std_ppcmds;
 
   (* Concerning a possible interface file *)
   sig_suffix : string option;
   (* the second argument is a comment to add to the preamble *)
-  sig_preamble : identifier -> std_ppcmds -> module_path list -> unsafe_needs -> std_ppcmds;
+  sig_preamble :
+    identifier -> std_ppcmds option -> module_path list -> unsafe_needs ->
+    std_ppcmds;
   pp_sig : ml_signature -> std_ppcmds;
 
   (* for an isolated declaration print *)
diff --git a/plugins/extraction/ocaml.ml b/plugins/extraction/ocaml.ml
index 826dcec02..7640416fd 100644
--- a/plugins/extraction/ocaml.ml
+++ b/plugins/extraction/ocaml.ml
@@ -63,8 +63,12 @@ let pp_open mp = str ("open "^ string_of_modfile mp ^"\n")
 
 let pp_comment s = str "(* " ++ hov 0 s ++ str " *)"
 
+let pp_header_comment = function
+  | None -> mt ()
+  | Some com -> pp_comment com ++ fnl () ++ fnl ()
+
 let preamble _ comment used_modules usf =
-  pp_comment comment ++ fnl () ++ fnl () ++
+  pp_header_comment comment ++
   prlist pp_open used_modules ++
   (if used_modules = [] then mt () else fnl ()) ++
   (if usf.tdummy || usf.tunknown then str "type __ = Obj.t\n" else mt()) ++
@@ -74,7 +78,7 @@ let preamble _ comment used_modules usf =
   (if usf.tdummy || usf.tunknown || usf.mldummy then fnl () else mt ())
 
 let sig_preamble _ comment used_modules usf =
-  pp_comment comment ++ fnl () ++ fnl () ++
+  pp_header_comment comment ++ fnl () ++ fnl () ++
   prlist pp_open used_modules ++
   (if used_modules = [] then mt () else fnl ()) ++
   (if usf.tdummy || usf.tunknown then str "type __ = Obj.t\n\n" else mt())
diff --git a/plugins/extraction/scheme.ml b/plugins/extraction/scheme.ml
index a0a59e73c..bfbcc7b0a 100644
--- a/plugins/extraction/scheme.ml
+++ b/plugins/extraction/scheme.ml
@@ -28,10 +28,14 @@ let keywords =
 
 let pp_comment s = str";; "++h 0 s++fnl ()
 
+let pp_header_comment = function
+  | None -> mt ()
+  | Some com -> pp_comment com ++ fnl () ++ fnl ()
+
 let preamble _ comment _ usf =
-  pp_comment comment ++ fnl () ++
+  pp_header_comment comment ++
   str ";; This extracted scheme code relies on some additional macros\n" ++
-  str ";; available at http://www.pps.jussieu.fr/~letouzey/scheme\n" ++
+  str ";; available at http://www.pps.univ-paris-diderot.fr/~letouzey/scheme\n" ++
   str "(load \"macros_extr.scm\")\n\n" ++
   (if usf.mldummy then str "(define __ (lambda (_) __))\n\n" else mt ())
 
@@ -224,7 +228,7 @@ let scheme_descr = {
   preamble = preamble;
   pp_struct = pp_struct;
   sig_suffix = None;
-  sig_preamble = (fun _ s _ _ -> pp_comment s ++ fnl () ++ fnl ());
+  sig_preamble = (fun _ _ _ _ -> mt ());
   pp_sig = (fun _ -> mt ());
   pp_decl = pp_decl;
 }