Skip to content
GitLab
Menu
Projects
Groups
Snippets
Loading...
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Menu
Open sidebar
pub
frama-c
Commits
9f3d8206
Commit
9f3d8206
authored
Apr 08, 2020
by
Michele Alberti
Browse files
[journal] Port to Filepath for session filename.
No internal representation change.
parent
d991ac9c
Changes
3
Hide whitespace changes
Inline
Side-by-side
src/kernel_services/plugin_entry_points/journal.ml
View file @
9f3d8206
...
...
@@ -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
;
...
...
src/kernel_services/plugin_entry_points/journal.mli
View file @
9f3d8206
...
...
@@ -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:
...
...
src/kernel_services/plugin_entry_points/plugin.ml
View file @
9f3d8206
...
...
@@ -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
...
...
Write
Preview
Markdown
is supported
0%
Try again
or
attach a new file
.
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment