Commit 4c022d64 authored by Guillaume Melquiond's avatar Guillaume Melquiond

Use restore_path systematically when merging theories (bug #20445).

When sessions are saved and then loaded from disk, goal identifiers are
properly qualified. This is not the case when goals are still in memory
due to reloading a file in the ide. So merging can get confused since
several goals potentially share the same base name.
parent e929c65f
......@@ -2364,9 +2364,13 @@ exception OutdatedSession
let merge_theory ~ctxt ~theories env from_th to_th =
found_missed_goals_in_theory := false;
set_theory_expanded to_th from_th.theory_expanded;
let get_goal_name g =
let (_,_,l) = restore_path g.goal_name in
String.concat "." l
with Not_found -> g.goal_name.Ident.id_string in
let from_goals = List.fold_left
(fun from_goals g ->
Mstr.add g.goal_name.Ident.id_string g from_goals)
(fun from_goals g -> Mstr.add (get_goal_name g) g from_goals)
Mstr.empty from_th.theory_goals
Debug.dprintf debug
......@@ -2377,16 +2381,11 @@ let merge_theory ~ctxt ~theories env from_th to_th =
(fun to_goal ->
let to_goal_name =
let (_,_,l) = restore_path to_goal.goal_name
in String.concat "." l
with Not_found -> to_goal.goal_name.Ident.id_string
let to_goal_name = get_goal_name to_goal in
let from_goal = Mstr.find to_goal_name from_goals in
Debug.dprintf debug
"[Goal checksum] goal %s: old sum = %a, new sum = %a@."
(Pp.print_option Tc.print_checksum) from_goal.goal_checksum
(Pp.print_option Tc.print_checksum) to_goal.goal_checksum;
let goal_obsolete =
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