diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2015-01-23 14:15:10 +0100 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2015-01-23 14:15:10 +0100 |
| commit | 4f632721be8b083126f49dd900a3294521879ec4 (patch) | |
| tree | b5e08036a9834f9e7331f5abbbb2da3c9a5cd72b /plugins/extraction/ocaml.ml | |
| parent | feca7916eaaceea96be4c15f08895578b3703a1c (diff) | |
Extraction: fix #3629.
The control flow of extraction is hard to read due to exceptions. When meeting
an inlined constant extracted to custom code, they could desynchronize some
tables in charge of detecting name clashes, leading to an anomaly.
Diffstat (limited to 'plugins/extraction/ocaml.ml')
| -rw-r--r-- | plugins/extraction/ocaml.ml | 10 |
1 files changed, 8 insertions, 2 deletions
diff --git a/plugins/extraction/ocaml.ml b/plugins/extraction/ocaml.ml index 30ac3d3f8..ce88ea6d2 100644 --- a/plugins/extraction/ocaml.ml +++ b/plugins/extraction/ocaml.ml @@ -634,7 +634,10 @@ and pp_module_type params = function str "functor (" ++ name ++ str ":" ++ typ ++ str ") ->" ++ fnl () ++ def | MTsig (mp, sign) -> push_visible mp params; - let l = List.map pp_specif sign in + let try_pp_specif x l = + try pp_specif x :: l with Failure "empty phrase" -> l + in + let l = List.fold_right try_pp_specif sign [] in pop_visible (); str "sig " ++ fnl () ++ v 1 (str " " ++ prlist_with_sep fnl2 identity l) ++ @@ -707,7 +710,10 @@ and pp_module_expr params = function str "functor (" ++ name ++ str ":" ++ typ ++ str ") ->" ++ fnl () ++ def | MEstruct (mp, sel) -> push_visible mp params; - let l = List.map pp_structure_elem sel in + let try_pp_structure_elem x l = + try pp_structure_elem x :: l with Failure "empty phrase" -> l + in + let l = List.fold_right try_pp_structure_elem sel [] in pop_visible (); str "struct " ++ fnl () ++ v 1 (str " " ++ prlist_with_sep fnl2 identity l) ++ |