Commit 804401a4 authored by François Bobot's avatar François Bobot

Session rewrite fix :

 - create a session if the directory doesn't exists
 - If the directory exists but the xml doesn't behave as if the xml is empty.
parent ee5d7269
......@@ -624,7 +624,9 @@ let () =
let env_session,sched =
try
eprintf "[Info] Opening session...@\n@[<v 2> ";
let session = S.read_session project_dir in
let session =
if Sys.file_exists project_dir then S.read_session project_dir
else S.create_session project_dir in
let env_session,(_:bool) =
M.update_session ~allow_obsolete:true session gconfig.env
gconfig.Gconfig.config
......
......@@ -865,23 +865,30 @@ let load_session session xml =
exception OpenError of string
type notask = unit
let read_session dir =
if not (Sys.file_exists dir && Sys.is_directory dir) then
raise (OpenError (Pp.sprintf "%s is not an existing directory" dir));
let xml_filename = Filename.concat dir db_filename in
let session = {session_files = PHstr.create 3; session_dir = dir} in
try
let xml = Xml.from_file (Filename.concat dir db_filename) in
(** If the xml is present we read it, otherwise we consider it empty *)
if Sys.file_exists xml_filename then begin
try
load_session session xml;
session
with Sys_error msg ->
failwith ("Open session: sys error " ^ msg)
with
| Sys_error _msg ->
(* xml does not exist yet *)
raise (OpenError "Can't open")
| Xml.Parse_error s ->
Format.eprintf "XML database corrupted, ignored (%s)@." s;
let xml = Xml.from_file xml_filename in
try
load_session session xml;
with Sys_error msg ->
failwith ("Open session: sys error " ^ msg)
with
| Sys_error _msg ->
(* xml does not exist yet *)
raise (OpenError "Can't open")
| Xml.Parse_error s ->
Format.eprintf "XML database corrupted, ignored (%s)@." s;
(* failwith
("Open session: XML database corrupted (%s)@." ^ s) *)
raise (OpenError "XML corrupted")
raise (OpenError "XML corrupted")
end;
session
(*******************************)
(* Session modification *)
......
......@@ -350,7 +350,8 @@ let redo_external_proof eS eT ?timelimit g a =
else
match load_prover eS a.proof_prover with
| None -> Debug.dprintf debug
"[Info] Can't redo an external proof since the prover %a is not loaded"
"[Info] Can't redo an external proof since the prover %a is not \
loaded@."
print_prover a.proof_prover
| Some p ->
if a.proof_edited_as = None && p.prover_config.Whyconf.interactive then
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment