From a8129c5ed3bc6622b3e8fe4d8545594a74af8e5b Mon Sep 17 00:00:00 2001
From: Andre Maroneze <andre.maroneze@cea.fr>
Date: Fri, 30 Apr 2021 18:09:18 +0200
Subject: [PATCH] [Journal] increase usage of normalized paths
---
.../plugin_entry_points/journal.ml | 16 +++++++++-------
.../plugin_entry_points/journal.mli | 4 ++--
2 files changed, 11 insertions(+), 9 deletions(-)
diff --git a/src/kernel_services/plugin_entry_points/journal.ml b/src/kernel_services/plugin_entry_points/journal.ml
index 630371b8ee7..b08df75e436 100644
--- a/src/kernel_services/plugin_entry_points/journal.ml
+++ b/src/kernel_services/plugin_entry_points/journal.ml
@@ -142,7 +142,7 @@ let print_trailer fmt =
Format.fprintf fmt "@[(* Main *)@]@\n";
Format.fprintf fmt "@[<hv 2>let main () =@;";
Format.fprintf fmt
- "@[<hv 0>@[<hv 2>Journal.keep_file@;\"%s\";@]@;"
+ "@[<hv 0>@[<hv 2>Journal.keep_file@; (Datatype.Filepath.of_string@; (\"%s\"));@]@;"
name;
Format.fprintf fmt "try run ()@;";
Format.fprintf fmt "@[<v>with@;@[<hv 2>| Unreachable ->@ ";
@@ -170,14 +170,15 @@ let print_trailer fmt =
(* close the outermost box *)
Format.pp_close_box fmt ()
-let preserved_files = ref []
+let preserved_files : Datatype.Filepath.t list ref = ref []
let keep_file s = preserved_files := s :: !preserved_files
let get_filename =
let cpt = ref 0 in
let rec get_filename first =
- let name = Format.asprintf "%a" Datatype.Filepath.pretty (get_name ()) in
- if (not first && Sys.file_exists name) || List.mem name !preserved_files
+ let name_fp = get_name () in
+ let name = (name_fp:>string) in
+ if (not first && Sys.file_exists name) || List.mem name_fp !preserved_files
then begin
incr cpt;
let suf = "_" ^ string_of_int !cpt in
@@ -193,7 +194,7 @@ let get_filename =
filename := name ^ suf);
get_filename false
end else
- name
+ name_fp
in
fun () -> get_filename true
@@ -208,9 +209,10 @@ let write () =
in
let error msg s = error "cannot %s journal (%s)." msg s in
let filename = get_filename () in
- feedback "writing journal in file `%s'." filename;
+ feedback "writing journal in file `%a'."
+ Datatype.Filepath.pretty filename;
try
- let cout = open_out filename in
+ let cout = open_out (filename:>string) in
let fmt = Format.formatter_of_out_channel cout in
Format.pp_set_margin fmt 78 (* line length *);
(try write fmt with Sys_error s -> error "write into" s);
diff --git a/src/kernel_services/plugin_entry_points/journal.mli b/src/kernel_services/plugin_entry_points/journal.mli
index b3e63d7548e..01fcade163a 100644
--- a/src/kernel_services/plugin_entry_points/journal.mli
+++ b/src/kernel_services/plugin_entry_points/journal.mli
@@ -106,8 +106,8 @@ val restore: unit -> unit
(** {2 Internal use only} *)
(* ****************************************************************************)
-val keep_file: string -> unit
-(** This function has not to be used explicitly. Only offers functions
+val keep_file: Datatype.Filepath.t -> unit
+(** This function is not to be used explicitly. Only offers functions
retrieving when running a journal file. *)
val get_session_file: (string -> Datatype.Filepath.t) ref
--
GitLab