Commit 98fca983 authored by Guillaume Melquiond's avatar Guillaume Melquiond
Browse files

Update tabs only after updating the name of the current file.

Otherwise tabs would be using the previous source file.
parent 4529867b
......@@ -2367,8 +2367,7 @@ let select_row r =
let ind = goals_model#get ~row:r#iter ~column:index_column in
current_selected_row := Some ind;
let a = get_any_from_row_reference r in
update_tabs a;
match a with
begin match a with
| S.Goal g ->
scroll_to_source_goal g
| S.Theory th ->
......@@ -2384,6 +2383,8 @@ let select_row r =
scroll_to_source_goal tr.S.transf_parent
| S.Metas m ->
scroll_to_source_goal m.S.metas_parent
update_tabs a
(* row selection on tree view on the left *)
let (_ : =
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