diff options
| author |  Cyprien Mangin <cyprien.mangin@m4x.org> | 2018-06-26 19:55:39 +0200 |
|---|---|---|
| committer | Cyprien Mangin <cyprien.mangin@m4x.org> | 2018-06-27 12:33:08 +0200 |
| commit | 77a1ea99faf980f7fe877e1bfb0460d53c58cc6f (patch) | |
| tree | 909548bdac9a82769285a1785431c7ee7db803c9 /ide | |
| parent | b98ae49d282f73343c1950e960f4b3bc7c28de70 (diff) | |
CoqIDE scrolls the proof buffer down to the first goal.
Diffstat (limited to 'ide')
| -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 | [] -> [] |