diff options
author | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2018-06-28 12:41:48 +0200 |
---|---|---|
committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2018-06-28 12:41:48 +0200 |
commit | 8117f98527169955086332d771b1201b8f98cf31 (patch) | |
tree | da7aa02cc7ebd91862510f3553f6c8a7ab1bf193 | |
parent | 809eaea3c179ca23036ae807e8f8c1a749a027f7 (diff) | |
parent | 77a1ea99faf980f7fe877e1bfb0460d53c58cc6f (diff) |
Merge PR #7932: CoqIDE scrolls the proof buffer down to the first goal.
-rw-r--r-- | ide/wg_ProofView.ml | 4 |
1 files changed, 2 insertions, 2 deletions
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 | [] -> [] |