diff --git a/src/kernel_services/plugin_entry_points/journal.ml b/src/kernel_services/plugin_entry_points/journal.ml index 52a50fb59f9411d409163dca940bdaaca5d2a8ae..9294d088ba416ff36858c5a21e8ca47ee4ffc9a8 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 33573824a5cf99e7ec2bdc783c4137723cd81a3a..82d2b8d6529890d0d9baa8a23ece895a8fdee601 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 667d8aeef6ee4b8acc24dc3a74e37ea632197395..4b7b4a2de3b925a0d3700d224e50f45bb70519a6 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