aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins
diff options
context:
space:
mode:
authorGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2012-10-30 14:16:06 +0000
committerGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2012-10-30 14:16:06 +0000
commita14e4c0670eda14686a6fcf24b909f9fc3e1e3d3 (patch)
tree893b2e601fd9b1f04ae17e3d79c69eff91213b42 /plugins
parent6cd21c58557309919083610caff4a0b65a5c041f (diff)
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
Diffstat (limited to 'plugins')
-rw-r--r--plugins/extraction/extract_env.ml16
-rw-r--r--plugins/extraction/haskell.ml6
-rw-r--r--plugins/extraction/miniml.mli8
-rw-r--r--plugins/extraction/ocaml.ml8
-rw-r--r--plugins/extraction/scheme.ml10
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;
}