[wp] differenciate report-in and report-out for json

src/plugins/wp/register.ml

@@ -139,13 +139,22 @@ let do_wp_print_for goals =
 
 let do_wp_report () =
   begin
-    let rfiles = Wp_parameters.Report.get () in
-    if rfiles <> [] then
+    let reports = Wp_parameters.Report.get () in
+    let jreport = Wp_parameters.ReportJson.get () in
+    if reports <> [] || jreport <> "" then
       begin
         let stats = WpReport.fcstat () in
-        let jfile = Wp_parameters.ReportJson.get () in
-        if jfile <> "" then WpReport.export_json stats jfile ;
-        List.iter (WpReport.export stats) rfiles ;
+        begin
+          match Transitioning.String.split_on_char ':' jreport with
+          | [] | [""] -> ()
+          | [joutput] ->
+              WpReport.export_json stats ~joutput () ;
+          | [jinput;joutput] ->
+              WpReport.export_json stats ~jinput ~joutput () ;
+          | _ ->
+              Wp_parameters.error "Invalid format for option -wp-report-json"
+        end ;
+        List.iter (WpReport.export stats) reports ;
       end ;
     if Wp_parameters.MemoryContext.get () then
       wp_warn_memory_context ()

src/plugins/wp/wpReport.ml

@@ -864,20 +864,29 @@ let export gstat specfile =
 
 (* -------------------------------------------------------------------------- *)
 
-let export_json gstat jfile =
+let export_json gstat ?jinput ~joutput () =
   begin
-    Wp_parameters.feedback "Report '%s'" jfile ;
     let js =
       try
-        if Sys.file_exists jfile
-        then Json.load_file jfile else `Null
+        let jfile = match jinput with
+          | None ->
+              Wp_parameters.feedback "Report '%s'" joutput ;
+              joutput
+          | Some jinput ->
+              Wp_parameters.feedback "Report in:  '%s'" jinput ;
+              Wp_parameters.feedback "Report out: '%s'" joutput ;
+              jinput
+        in
+        if Sys.file_exists jfile then
+          Json.load_file jfile
+        else `Null
       with Json.Error(file,line,msg) ->
         let source = Log.source ~file ~line in
         Wp_parameters.error ~source "Incorrect json file: %s" msg ;
         `Null
     in
     rankify_fcstat gstat js ;
-    Json.save_file jfile (json_of_fcstat gstat) ;
+    Json.save_file joutput (json_of_fcstat gstat) ;
   end
 
 

src/plugins/wp/wpReport.mli

@@ -47,4 +47,4 @@ type fcstat
 val fcstat : unit -> fcstat
 
 val export : fcstat -> string -> unit
-val export_json : fcstat -> string -> unit
+val export_json : fcstat -> ?jinput:string -> joutput:string -> unit -> unit