diff options
author | aspiwack <aspiwack@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-08-24 17:36:36 +0000 |
---|---|---|
committer | aspiwack <aspiwack@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-08-24 17:36:36 +0000 |
commit | 7993d50d0d1dd029b34745e1ee089d9cf7c5ffbd (patch) | |
tree | c63659baaa5fbb525c6fc1cb4ad882e8e6b55e1c /plugins/extraction/extract_env.ml | |
parent | 6a2f9c59ea44d754050b4a2ccb624adcc846924d (diff) |
Experimental support for a comment in the files' preamble in extraction.
Scheme comments are output on a single line because Ocaml's Format
module which serves as a backend to Pp has an integer, rather than a string
as identation value, so we cannot make it so that each new line in the
comment starts with ";; ".
I've tried something with Pp.ifb but it was hackish at best and had somewhat
strange results.
Known bug: as Pp.std_ppcmds is non-persistent, the comment is actually printed
only once per Extraction command, even if it outputs several files.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15763 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'plugins/extraction/extract_env.ml')
-rw-r--r-- | plugins/extraction/extract_env.ml | 8 |
1 files changed, 6 insertions, 2 deletions
diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml index 292ae7955..588fe0cf2 100644 --- a/plugins/extraction/extract_env.ml +++ b/plugins/extraction/extract_env.ml @@ -470,10 +470,14 @@ 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 begin try (* The real printing of the implementation *) set_phase Impl; - pp_with ft (d.preamble mo opened unsafe_needs); + pp_with ft (d.preamble mo file_comment opened unsafe_needs); pp_with ft (d.pp_struct struc); Option.iter close_out cout; with e -> @@ -487,7 +491,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 opened unsafe_needs); + pp_with ft (d.sig_preamble mo file_comment opened unsafe_needs); pp_with ft (d.pp_sig (signature_of_structure struc)); close_out cout; with e -> |