Commit ce484aa2 authored by Sylvain Dailler's avatar Sylvain Dailler

session loading: fix the default format of files

When the format is not present, we use the extension of the file to
generate it.
This fixes a problem that occured in Python files when old sessions were
kept, the file would become not parsable.
parent de05b2c9
......@@ -1205,8 +1205,8 @@ let load_theory ~version session parent_name old_provers (path,acc) th =
let load_file ~version session old_provers f =
match with
| "file" ->
(* This "name" attribute only exists in old sessions *)
let fn = string_attribute_opt "name" f in
let fmt = string_attribute_def "format" f Lexer.whyml_format in
let fid = gen_fileID session in
let path,ft =
......@@ -1222,6 +1222,12 @@ let load_file ~version session old_provers f =
| None -> assert false
else path
let fmt =
(* If the session is ill-formed and the format is absent, we use the
extension to decide the format *)
let def_fmt =
Env.get_format (Format.asprintf "%a" Sysutil.print_file_path path) in
string_attribute_def "format" f def_fmt in
let mf = { file_id = fid;
file_path = path;
file_format = fmt;
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