aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
-rw-r--r--plugins/extraction/extract_env.ml2
-rw-r--r--plugins/extraction/ocaml.ml19
2 files changed, 13 insertions, 8 deletions
diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml
index 3d32398ff..7014df83f 100644
--- a/plugins/extraction/extract_env.ml
+++ b/plugins/extraction/extract_env.ml
@@ -458,7 +458,7 @@ let print_one_decl struc mp decl =
push_visible mp [];
let ans = d.pp_decl decl in
pop_visible ();
- ans
+ v 0 ans
(*s Extraction of a ml struct to a file. *)
diff --git a/plugins/extraction/ocaml.ml b/plugins/extraction/ocaml.ml
index 7efe0b4e1..6ff4c25ec 100644
--- a/plugins/extraction/ocaml.ml
+++ b/plugins/extraction/ocaml.ml
@@ -388,9 +388,14 @@ and pp_fix par env i (ids,bl) args =
fnl () ++
hov 2 (str "in " ++ pp_apply (pr_id ids.(i)) false args)))
+(* Ad-hoc double-newline in v boxes, with enough negative whitespace
+ to avoid indenting the intermediate blank line *)
+
+let cut2 () = brk (0,-100000) ++ brk (0,0)
+
let pp_val e typ =
hov 4 (str "(** val " ++ e ++ str " :" ++ spc () ++ pp_type false [] typ ++
- str " **)") ++ fnl2 ()
+ str " **)") ++ cut2 ()
(*s Pretty-printing of [Dfix] *)
@@ -411,7 +416,7 @@ let pp_Dfix (rv,c,t) =
if is_custom rv.(i) then str " = " ++ str (find_custom rv.(i))
else pp_function (empty_env ()) c.(i)
in
- (if init then mt () else fnl2 ()) ++
+ (if init then mt () else cut2 ()) ++
pp_val names.(i) t.(i) ++
str (if init then "let rec " else "and ") ++ names.(i) ++ def ++
pp false (i+1)
@@ -644,7 +649,7 @@ and pp_module_type params = function
let l = List.rev l in
pop_visible ();
str "sig" ++ fnl () ++
- v 1 (str " " ++ prlist_with_sep fnl2 identity l) ++
+ v 1 (str " " ++ prlist_with_sep cut2 identity l) ++
fnl () ++ str "end"
| MTwith(mt,ML_With_type(idl,vl,typ)) ->
let ids = pp_parameters (rename_tvars keywords vl) in
@@ -723,7 +728,7 @@ and pp_module_expr params = function
let l = List.rev l in
pop_visible ();
str "struct" ++ fnl () ++
- v 1 (str " " ++ prlist_with_sep fnl2 identity l) ++
+ v 1 (str " " ++ prlist_with_sep cut2 identity l) ++
fnl () ++ str "end"
let rec prlist_sep_nonempty sep f = function
@@ -738,14 +743,14 @@ let rec prlist_sep_nonempty sep f = function
let do_struct f s =
let ppl (mp,sel) =
push_visible mp [];
- let p = prlist_sep_nonempty fnl2 f sel in
+ let p = prlist_sep_nonempty cut2 f sel in
(* for monolithic extraction, we try to simulate the unavailability
of [MPfile] in names by artificially nesting these [MPfile] *)
(if modular () then pop_visible ()); p
in
- let p = prlist_sep_nonempty fnl2 ppl s in
+ let p = prlist_sep_nonempty cut2 ppl s in
(if not (modular ()) then repeat (List.length s) pop_visible ());
- p ++ fnl ()
+ v 0 p ++ fnl ()
let pp_struct s = do_struct pp_structure_elem s