Bug fixed: "open X" were not printed in .mli because streams are destructive.

[helm.git] / matita / components / ng_extraction / ocamlExtraction.ml

diff --git a/matita/components/ng_extraction/ocamlExtraction.ml b/matita/components/ng_extraction/ocamlExtraction.ml
index 0022599a8dd4c503508a7f6ddceeaa025faf9fd0..6465aa86d26a57e9f68dcf30e640db202e792ed3 100644 (file)
--- a/matita/components/ng_extraction/ocamlExtraction.ml
+++ b/matita/components/ng_extraction/ocamlExtraction.ml
@@ -14,12 +14,13 @@ let print_ocaml_of_obj0 status ((_uri,_,_,_,_) as obj) =
    map_status status
     (fun status ml ->
       let status,cmds = Ocaml.pp_decl status ml in
-      print_ppcmds ~in_ml:true status (cmds ++ fnl ());
+      print_ppcmds ~in_ml:true status (cmds ++ fnl () ++ fnl ());
       status,()) res in
   status
  with
-  HExtlib.Localized (_,exn) ->
-   prerr_endline (Printexc.to_string exn); assert false
+    HExtlib.Localized (_,exn)
+  | exn ->
+     prerr_endline (Printexc.to_string exn); assert false
 
 let do_if_ocaml_set f status =
  if try ignore (Helm_registry.get "extract_ocaml"); true
@@ -40,6 +41,7 @@ let print_open status uris =
      List.map (fun uri -> Filename.basename (NUri.string_of_uri uri)) uris in
     let status,cmds = map_status status Ocaml.pp_open fnames in
     List.iter (print_ppcmds status ~in_ml:true) cmds;
+    let status,cmds = map_status status Ocaml.pp_open fnames in
     List.iter (print_ppcmds status ~in_ml:false) cmds;
     status
   ) status