Coqide Proofview scroll

 so that end of the corrent goal is the last visible line.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15173 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 7 insertions, 5 deletions

diff --git a/ide/ideproof.ml b/ide/ideproof.ml
index cb254a01ba..1e0f526a07 100644
--- a/ide/ideproof.ml
+++ b/ide/ideproof.ml
@@ -76,14 +76,15 @@ let mode_tactic sel_cb (proof:GText.view) goals hints = match goals with
       let () = proof#buffer#insert head_str in
       let () = insert_hyp hyps_hints hyps in
       let () =
-        let tags = if goal_hints <> [] then
+        let tags = Tags.Proof.goal :: if goal_hints <> [] then
           let tag = proof#buffer#create_tag [] in
           let () = hook_tag_cb tag goal_hints sel_cb on_hover in
           [tag]
           else []
         in
         proof#buffer#insert (goal_str 1 goals_cnt);
-        proof#buffer#insert ~tags (cur_goal ^ "\n")
+        proof#buffer#insert ~tags cur_goal;
+	proof#buffer#insert "\n"
       in
       (* Insert remaining goals (no hypotheses) *)
       let fold_goal i _ { Interface.goal_ccl = g } =
@@ -91,10 +92,11 @@ let mode_tactic sel_cb (proof:GText.view) goals hints = match goals with
         proof#buffer#insert (g ^ "\n")
       in
       let () = Minilib.list_fold_left_i fold_goal 2 () rem_goals in
-      ignore(proof#buffer#place_cursor  
-        ~where:((proof#buffer#get_iter_at_mark `INSERT)#backward_lines (3*goals_cnt - 2)));
-      ignore(proof#scroll_to_mark `INSERT)
 
+      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)
 
 let mode_cesar (proof:GText.view) = function
   | [] -> assert false