why3session info : add --edited-files option which

print all the edited files which appear in the session.

In conjonction with --print0 which prints '\000' instead of '\n' that
give a safe way to "git add" all the edited files of a session:

why3session info --edited-files --print0 vstte12_bfs.mlw |xargs -0 git add

Since why3session accept the why3session.xml (it uses the basename as
 session directory) you can add all the edited file of all the session
saved in a git repository with:

git ls-files -z |grep -z -e "why3session.xml$" |xargs -0 why3session info --edited-files --print0 | xargs -0 git add

src/session/session.ml

@@ -565,6 +565,9 @@ let set_obsolete ?(notify=notify) a =
 
 let set_archived a b = a.proof_archived <- b
 
+let get_edited_as_abs session pr =
+  option_map (Filename.concat session.session_dir) pr.proof_edited_as
+
 (* [raw_add_goal parent name expl sum t] adds a goal to the given parent
    DOES NOT record the new goal in its parent, thus this should not be exported
 *)

src/session/session.mli

@@ -279,6 +279,9 @@ val set_archived : 'key proof_attempt -> bool -> unit
 
 val set_edited_as : string option -> 'key proof_attempt -> unit
 
+val get_edited_as_abs : 'key session -> 'k proof_attempt -> string option
+(** return the edited filename after concatenation to session_dir *)
+
 val update_edit_external_proof :
   'key env_session -> 'key proof_attempt -> string
 (** return the absolute path of the edited file update with the

src/util/pp.ml

@@ -100,6 +100,7 @@ let rchevron fmt () = fprintf fmt ">"
 let nothing _fmt _ = ()
 let string fmt s = fprintf fmt "%s" s
 let constant_string s fmt () = string fmt s
+let print0 fmt () = pp_print_string fmt "\000"
 let add_flush sep fmt x = sep fmt x; pp_print_flush fmt ()
 
 let print_pair pr1 = print_pair_delim lparen comma rparen pr1

src/util/pp.mli

@@ -101,6 +101,7 @@ val rchevron : formatter -> unit -> unit
 val nothing : formatter -> 'a -> unit
 val string : formatter -> string -> unit
 val constant_string : string -> formatter -> unit -> unit
+val print0 : formatter -> unit -> unit
 val hov : int -> formatter -> ('a -> unit) -> 'a -> unit
 val add_flush : (formatter -> 'a -> unit) -> formatter -> 'a -> unit
 

src/why3session/why3session_info.ml

@@ -24,26 +24,40 @@ open Format
 module S = Session
 
 let opt_print_provers = ref false
+let opt_print_edited = ref false
 let opt_tree_print = ref false
 let opt_project_dir = ref false
+let opt_print0 = ref false
 
 let spec =
   ("--provers", Arg.Set opt_print_provers,
    " the prover used in the session are listed" ) ::
+  ("--edited-files", Arg.Set opt_print_edited,
+   " the edited files used in the session are listed" ) ::
   ("--tree", Arg.Set opt_tree_print,
    " the session is pretty printed in an ascii tree format" ) ::
   ("--dir", Arg.Set opt_project_dir,
    " print the directory of the session" ) ::
+  ("--print0", Arg.Set opt_print0,
+   " use the null character instead of newline to separate the output of \
+--provers and --edited-files" ) ::
   simple_spec
 
 let run_one fname =
   let project_dir = Session.get_project_dir fname in
   if !opt_project_dir then printf "%s@." project_dir;
   let session = Session.read_session project_dir in
+  let sep = if !opt_print0 then Pp.print0 else Pp.newline in
   if !opt_print_provers then
     printf "%a@."
-      (Pp.print_iter1 Sprover.iter Pp.newline print_prover)
+      (Pp.print_iter1 Sprover.iter sep print_prover)
       (S.get_used_provers session);
+  if !opt_print_edited then
+    S.session_iter_proof_attempt
+      (fun pr ->
+        Util.option_iter (fun s -> printf "%s%a" s sep ())
+          (S.get_edited_as_abs session pr))
+      session;
   if !opt_tree_print then
     printf "%a@." S.print_session session