Commit 95edf23e authored by Raphael Rieu-Helft's avatar Raphael Rieu-Helft

Read session proved status fromXML (total time still TODO), fix #82

parent fbacc121
......@@ -1090,6 +1090,8 @@ let load_theory session parent_name old_provers acc th =
List.iter2
(load_goal session old_provers (Theory mth))
th.Xml.elements goals;
let proved = bool_attribute "proved" th false in
Hid.add session.th_state thname proved;
mth::acc
| s ->
Warning.emit "[Warning] Session.load_theory: unexpected element '%s'@."
......
......@@ -202,7 +202,7 @@ let rec num_lines s acc tr =
(color_of_status ~dark:true) (th_proved s th)
name;
if th_proved s th then
fprintf fmt "fully verified in %%.02f s"
fprintf fmt "fully verified" (*TODO in %%.02f s*)
else fprintf fmt "not fully verified";
fprintf fmt "</span></h2>@\n";
......
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