From 9f3d8206a18fbce9ffefb7ec707d0352386983dc Mon Sep 17 00:00:00 2001
From: Michele Alberti <michele.alberti@cea.fr>
Date: Wed, 8 Apr 2020 10:29:35 +0200
Subject: [PATCH] [journal] Port to Filepath for session filename.
No internal representation change.
---
src/kernel_services/plugin_entry_points/journal.ml | 13 ++++++++-----
src/kernel_services/plugin_entry_points/journal.mli | 4 ++--
src/kernel_services/plugin_entry_points/plugin.ml | 6 +-----
3 files changed, 11 insertions(+), 12 deletions(-)
diff --git a/src/kernel_services/plugin_entry_points/journal.ml b/src/kernel_services/plugin_entry_points/journal.ml
index 52a50fb59f9..9294d088ba4 100644
--- a/src/kernel_services/plugin_entry_points/journal.ml
+++ b/src/kernel_services/plugin_entry_points/journal.ml
@@ -113,9 +113,11 @@ let now () = Unix.localtime (Unix.time ())
let default_filename = "frama_c_journal.ml"
let filename = ref default_filename
let get_session_file = ref (fun _ -> assert false)
-let get_name () =
+let get_name () =
let f = !filename in
- if f == default_filename then !get_session_file f else f
+ if f == default_filename
+ then !get_session_file f
+ else Datatype.Filepath.of_string f
let set_name s = filename := s
@@ -136,11 +138,12 @@ let print_header fmt =
"(* Run the user commands *)@;@[<hv 2>let run () =@;@[<hv 0>"
let print_trailer fmt =
+ let name = Format.asprintf "%a" Datatype.Filepath.pretty (get_name ()) in
Format.fprintf fmt "@[(* Main *)@]@\n";
Format.fprintf fmt "@[<hv 2>let main () =@;";
Format.fprintf fmt
"@[<hv 0>@[<hv 2>Journal.keep_file@;\"%s\";@]@;"
- (get_name ());
+ name;
Format.fprintf fmt "try run ()@;";
Format.fprintf fmt "@[<v>with@;@[<hv 2>| Unreachable ->@ ";
Format.fprintf fmt
@@ -155,7 +158,7 @@ let print_trailer fmt =
Format.fprintf fmt "@[(* Registering *)@]@\n";
Format.fprintf fmt
"@[<hv 2>let main : unit -> unit =@;@[<hv 2>Dynamic.register@;~plugin:%S@;\"main\"@;"
- (String.capitalize_ascii (Filename.basename (get_name ())));
+ (String.capitalize_ascii (Filename.basename name));
Format.fprintf fmt
"@[<hv 2>(Datatype.func@;Datatype.unit@;Datatype.unit)@]@;";
Format.fprintf fmt "~journalize:false@;main@]@]@\n@\n";
@@ -173,7 +176,7 @@ let keep_file s = preserved_files := s :: !preserved_files
let get_filename =
let cpt = ref 0 in
let rec get_filename first =
- let name = get_name () in
+ let name = Format.asprintf "%a" Datatype.Filepath.pretty (get_name ()) in
if (not first && Sys.file_exists name) || List.mem name !preserved_files
then begin
incr cpt;
diff --git a/src/kernel_services/plugin_entry_points/journal.mli b/src/kernel_services/plugin_entry_points/journal.mli
index 33573824a5c..82d2b8d6529 100644
--- a/src/kernel_services/plugin_entry_points/journal.mli
+++ b/src/kernel_services/plugin_entry_points/journal.mli
@@ -83,7 +83,7 @@ end
(** {2 Journal management} *)
(* ****************************************************************************)
-val get_name: unit -> string
+val get_name: unit -> Datatype.Filepath.t
(** @return the filename which the journal will be written into. *)
val set_name: string -> unit
@@ -110,7 +110,7 @@ val keep_file: string -> unit
(** This function has not to be used explicitly. Only offers functions
retrieving when running a journal file. *)
-val get_session_file: (string -> string) ref
+val get_session_file: (string -> Datatype.Filepath.t) ref
(*
Local Variables:
diff --git a/src/kernel_services/plugin_entry_points/plugin.ml b/src/kernel_services/plugin_entry_points/plugin.ml
index 667d8aeef6e..4b7b4a2de3b 100644
--- a/src/kernel_services/plugin_entry_points/plugin.ml
+++ b/src/kernel_services/plugin_entry_points/plugin.ml
@@ -417,11 +417,7 @@ struct
end)
let () =
if is_kernel ()
- then
- Journal.get_session_file :=
- (fun s ->
- let f = Session.file ~error:false s in
- Format.asprintf "%a" Datatype.Filepath.pretty f)
+ then Journal.get_session_file := (fun s -> Session.file ~error:false s)
module Config =
Make_specific_dir
--
GitLab