From 77a1ea99faf980f7fe877e1bfb0460d53c58cc6f Mon Sep 17 00:00:00 2001 From: Cyprien Mangin Date: Tue, 26 Jun 2018 19:55:39 +0200 Subject: CoqIDE scrolls the proof buffer down to the first goal. --- ide/wg_ProofView.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'ide') diff --git a/ide/wg_ProofView.ml b/ide/wg_ProofView.ml index b3088ee28..9be562d3e 100644 --- a/ide/wg_ProofView.ml +++ b/ide/wg_ProofView.ml @@ -103,7 +103,7 @@ let mode_tactic sel_cb (proof : #GText.view_skel) goals ~unfoc_goals hints = mat else [] in proof#buffer#insert (goal_str ~shownum:true 1 goals_cnt); - insert_xml proof#buffer (Richpp.richpp_of_pp width cur_goal); + insert_xml ~tags:[Tags.Proof.goal] proof#buffer (Richpp.richpp_of_pp width cur_goal); proof#buffer#insert "\n" in (* Insert remaining goals (no hypotheses) *) @@ -128,7 +128,7 @@ let mode_tactic sel_cb (proof : #GText.view_skel) goals ~unfoc_goals hints = mat ignore(proof#buffer#place_cursor ~where:(proof#buffer#end_iter#backward_to_tag_toggle (Some Tags.Proof.goal))); - ignore(proof#scroll_to_mark ~use_align:true ~yalign:0.95 `INSERT) + ignore(proof#scroll_to_mark `INSERT) let rec flatten = function | [] -> [] -- cgit v1.2.3