Commit 2d066743 authored by MARCHE Claude's avatar MARCHE Claude

recover explanations properly on session reload

parent c71c9208
...@@ -587,9 +587,9 @@ let mk_proof_node ~shape_version ~expl (s : session) (n : Ident.ident) (t : Task ...@@ -587,9 +587,9 @@ let mk_proof_node ~shape_version ~expl (s : session) (n : Ident.ident) (t : Task
let mk_new_proof_node = mk_proof_node ~shape_version:Termcode.current_shape_version let mk_new_proof_node = mk_proof_node ~shape_version:Termcode.current_shape_version
let mk_proof_node_no_task (s : session) (n : Ident.ident) let mk_proof_node_no_task (s : session) (n : Ident.ident)
(parent : proof_parent) (node_id : proofNodeID) sum shape proved = (parent : proof_parent) (node_id : proofNodeID) sum shape expl proved =
let pn = { proofn_name = n; let pn = { proofn_name = n;
proofn_expl = ""; proofn_expl = expl;
proofn_parent = parent; proofn_parent = parent;
proofn_attempts = Hprover.create 7; proofn_attempts = Hprover.create 7;
proofn_transformations = [] } in proofn_transformations = [] } in
...@@ -999,8 +999,9 @@ let rec load_goal session old_provers parent g id = ...@@ -999,8 +999,9 @@ let rec load_goal session old_provers parent g id =
try Termcode.shape_of_string (List.assoc "shape" g.Xml.attributes) try Termcode.shape_of_string (List.assoc "shape" g.Xml.attributes)
with Not_found -> Termcode.shape_of_string "" with Not_found -> Termcode.shape_of_string ""
in in
let expl = string_attribute_def "expl" g "" in
let proved = bool_attribute "proved" g false in let proved = bool_attribute "proved" g false in
mk_proof_node_no_task session gname parent id sum shape proved; mk_proof_node_no_task session gname parent id sum shape expl proved;
List.iter (load_proof_or_transf session old_provers id) g.Xml.elements; List.iter (load_proof_or_transf session old_provers id) g.Xml.elements;
| "label" -> () | "label" -> ()
| s -> | s ->
...@@ -1307,13 +1308,14 @@ let save_detached_proof s parent old_pa_n = ...@@ -1307,13 +1308,14 @@ let save_detached_proof s parent old_pa_n =
let rec save_detached_goal old_s s parent detached_goal_id id = let rec save_detached_goal old_s s parent detached_goal_id id =
let detached_goal = get_proofNode old_s detached_goal_id in let detached_goal = get_proofNode old_s detached_goal_id in
let (sum,shape) = Hpn.find old_s.session_sum_shape_table detached_goal_id in let (sum,shape) = Hpn.find old_s.session_sum_shape_table detached_goal_id in
mk_proof_node_no_task s detached_goal.proofn_name parent id sum shape false; mk_proof_node_no_task s detached_goal.proofn_name parent id sum shape
Hprover.iter (fun _ pa -> detached_goal.proofn_expl false;
let pa = get_proof_attempt_node old_s pa in Hprover.iter (fun _ pa ->
save_detached_proof s id pa) detached_goal.proofn_attempts; let pa = get_proof_attempt_node old_s pa in
List.iter (save_detached_trans old_s s id) detached_goal.proofn_transformations; save_detached_proof s id pa) detached_goal.proofn_attempts;
let new_trans = (get_proofNode s id) in List.iter (save_detached_trans old_s s id) detached_goal.proofn_transformations;
new_trans.proofn_transformations <- List.rev new_trans.proofn_transformations let new_trans = (get_proofNode s id) in
new_trans.proofn_transformations <- List.rev new_trans.proofn_transformations
and save_detached_goals old_s detached_goals_id s parent = and save_detached_goals old_s detached_goals_id s parent =
......
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