diff options
author | Maxime Dénès <mail@maximedenes.fr> | 2017-03-24 16:15:32 +0100 |
---|---|---|
committer | Maxime Dénès <mail@maximedenes.fr> | 2017-03-24 16:15:32 +0100 |
commit | af291869bb7d1184d8e655906572d75937ca829b (patch) | |
tree | 62a5ccf9ee7b115b7d1118cbc3db92c553261713 /plugins/extraction | |
parent | 3234a893a1b3cfd6b51f1c26cc10e9690d8a703e (diff) | |
parent | 7535e268f7706d1dee263fdbafadf920349103db (diff) |
Merge branch 'trunk' into pr379
Diffstat (limited to 'plugins/extraction')
-rw-r--r-- | plugins/extraction/common.ml | 9 | ||||
-rw-r--r-- | plugins/extraction/extract_env.ml | 9 | ||||
-rw-r--r-- | plugins/extraction/g_extraction.ml4 | 1 | ||||
-rw-r--r-- | plugins/extraction/ocaml.ml | 8 | ||||
-rw-r--r-- | plugins/extraction/scheme.ml | 6 | ||||
-rw-r--r-- | plugins/extraction/table.ml | 4 |
6 files changed, 18 insertions, 19 deletions
diff --git a/plugins/extraction/common.ml b/plugins/extraction/common.ml index de97ba97c..fc8d5356c 100644 --- a/plugins/extraction/common.ml +++ b/plugins/extraction/common.ml @@ -67,7 +67,9 @@ let pp_boxed_tuple f = function blocks is less that a line length. To avoid this awkward situation, we attach a big virtual size to [fnl] newlines. *) -let fnl () = stras (1000000,"") ++ fnl () +(* EG: This looks quite suspicious... but beware of bugs *) +(* let fnl () = stras (1000000,"") ++ fnl () *) +let fnl () = fnl () let fnl2 () = fnl () ++ fnl () @@ -91,10 +93,7 @@ let begins_with_CoqXX s = let unquote s = if lang () != Scheme then s - else - let s = String.copy s in - for i=0 to String.length s - 1 do if s.[i] == '\'' then s.[i] <- '~' done; - s + else String.map (fun c -> if c == '\'' then '~' else c) s let rec qualify delim = function | [] -> assert false diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml index e019bb3c2..2b12462ad 100644 --- a/plugins/extraction/extract_env.ml +++ b/plugins/extraction/extract_env.ml @@ -472,13 +472,14 @@ let formatter dry file = if dry then Format.make_formatter (fun _ _ _ -> ()) (fun _ -> ()) else match file with - | Some f -> Pp_control.with_output_to f + | Some f -> Topfmt.with_output_to f | None -> Format.formatter_of_buffer buf in + (* XXX: Fixme, this shouldn't depend on Topfmt *) (* We never want to see ellipsis ... in extracted code *) Format.pp_set_max_boxes ft max_int; (* We reuse the width information given via "Set Printing Width" *) - (match Pp_control.get_margin () with + (match Topfmt.get_margin () with | None -> () | Some i -> Format.pp_set_margin ft i; @@ -518,8 +519,10 @@ let print_structure_to_file (fn,si,mo) dry struc = set_phase Impl; pp_with ft (d.preamble mo comment opened unsafe_needs); pp_with ft (d.pp_struct struc); + Format.pp_print_flush ft (); Option.iter close_out cout; with reraise -> + Format.pp_print_flush ft (); Option.iter close_out cout; raise reraise end; if not dry then Option.iter info_file fn; @@ -532,8 +535,10 @@ let print_structure_to_file (fn,si,mo) dry struc = set_phase Intf; pp_with ft (d.sig_preamble mo comment opened unsafe_needs); pp_with ft (d.pp_sig (signature_of_structure struc)); + Format.pp_print_flush ft (); close_out cout; with reraise -> + Format.pp_print_flush ft (); close_out cout; raise reraise end; info_file si) diff --git a/plugins/extraction/g_extraction.ml4 b/plugins/extraction/g_extraction.ml4 index e1d6bb4a8..3ed959cf2 100644 --- a/plugins/extraction/g_extraction.ml4 +++ b/plugins/extraction/g_extraction.ml4 @@ -12,6 +12,7 @@ DECLARE PLUGIN "extraction_plugin" (* ML names *) +open Ltac_plugin open Genarg open Stdarg open Pcoq.Prim diff --git a/plugins/extraction/ocaml.ml b/plugins/extraction/ocaml.ml index d89bf95ee..d8e382155 100644 --- a/plugins/extraction/ocaml.ml +++ b/plugins/extraction/ocaml.ml @@ -66,7 +66,7 @@ let pp_header_comment = function | None -> mt () | Some com -> pp_comment com ++ fnl2 () -let then_nl pp = if Pp.is_empty pp then mt () else pp ++ fnl () +let then_nl pp = if Pp.ismt pp then mt () else pp ++ fnl () let pp_tdummy usf = if usf.tdummy || usf.tunknown then str "type __ = Obj.t" ++ fnl () else mt () @@ -618,7 +618,7 @@ and pp_module_type params = function push_visible mp params; let try_pp_specif l x = let px = pp_specif x in - if Pp.is_empty px then l else px::l + if Pp.ismt px then l else px::l in (* We cannot use fold_right here due to side effects in pp_specif *) let l = List.fold_left try_pp_specif [] sign in @@ -696,7 +696,7 @@ and pp_module_expr params = function push_visible mp params; let try_pp_structure_elem l x = let px = pp_structure_elem x in - if Pp.is_empty px then l else px::l + if Pp.ismt px then l else px::l in (* We cannot use fold_right here due to side effects in pp_structure_elem *) let l = List.fold_left try_pp_structure_elem [] sel in @@ -714,7 +714,7 @@ let rec prlist_sep_nonempty sep f = function | h::t -> let e = f h in let r = prlist_sep_nonempty sep f t in - if Pp.is_empty e then r + if Pp.ismt e then r else e ++ sep () ++ r let do_struct f s = diff --git a/plugins/extraction/scheme.ml b/plugins/extraction/scheme.ml index a6309e61f..8d0cc4a0d 100644 --- a/plugins/extraction/scheme.ml +++ b/plugins/extraction/scheme.ml @@ -40,11 +40,7 @@ let preamble _ comment _ usf = (if usf.mldummy then str "(define __ (lambda (_) __))\n\n" else mt ()) let pr_id id = - let s = Id.to_string id in - for i = 0 to String.length s - 1 do - if s.[i] == '\'' then s.[i] <- '~' - done; - str s + str @@ String.map (fun c -> if c == '\'' then '~' else c) (Id.to_string id) let paren = pp_par true diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml index 5e7d810c9..d6a334c5f 100644 --- a/plugins/extraction/table.ml +++ b/plugins/extraction/table.ml @@ -773,9 +773,7 @@ let file_of_modfile mp = | MPfile f -> Id.to_string (List.hd (DirPath.repr f)) | _ -> assert false in - let s = String.copy (string_of_modfile mp) in - if s.[0] != s0.[0] then s.[0] <- s0.[0]; - s + String.mapi (fun i c -> if i = 0 then s0.[0] else c) (string_of_modfile mp) let add_blacklist_entries l = blacklist_table := |