Return of the tactic hints features in CoqIDE.

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

4 files changed, 44 insertions, 28 deletions

diff --git a/ide/coq.ml b/ide/coq.ml
index 93eac0962e..8c2e7105ce 100644
--- a/ide/coq.ml
+++ b/ide/coq.ml
@@ -214,6 +214,7 @@ let rewind coqtop i = eval_call coqtop (Ide_intf.rewind i)
 let inloadpath coqtop s = eval_call coqtop (Ide_intf.inloadpath s)
 let mkcases coqtop s = eval_call coqtop (Ide_intf.mkcases s)
 let status coqtop = eval_call coqtop Ide_intf.status
+let hints coqtop = eval_call coqtop Ide_intf.hints
 
 module PrintOpt =
 struct
diff --git a/ide/coq.mli b/ide/coq.mli
index b3b51d3fcf..3a92646500 100644
--- a/ide/coq.mli
+++ b/ide/coq.mli
@@ -50,6 +50,7 @@ val interp :
 val rewind : coqtop -> int -> int Ide_intf.value
 val status : coqtop -> Ide_intf.status Ide_intf.value
 val goals : coqtop -> Ide_intf.goals Ide_intf.value
+val hints : coqtop -> (Ide_intf.hint list * Ide_intf.hint) option Ide_intf.value
 val inloadpath : coqtop -> string -> bool Ide_intf.value
 val mkcases : coqtop -> string -> string list list Ide_intf.value
 
diff --git a/ide/coqide.ml b/ide/coqide.ml
index d224e72b56..3e87ad3683 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -833,9 +833,13 @@ object(self)
           | Ide_intf.Fail (l,str) ->
             self#set_message ("Error in coqtop :\n"^str)
           | Ide_intf.Good goals ->
+            let hints = match Coq.hints !mycoqtop with
+            | Ide_intf.Fail (_, _) -> None
+            | Ide_intf.Good hints -> hints
+            in
             Ideproof.display
               (Ideproof.mode_tactic menu_callback)
-              proof_view goals
+              proof_view goals hints
       with
         | e -> prerr_endline (Printexc.to_string e)
     end
@@ -2924,9 +2928,6 @@ let read_coqide_args argv =
       if coqtop = "" then filter_coqtop prog project_files out args
       else
 	(output_string stderr "Error: multiple -coqtop options"; exit 1)
-    | "-debug" :: args ->
-      Ideutils.debug := true;
-      filter_coqtop coqtop project_files ("-debug"::out) args
     | "-f" :: file :: args ->
 	filter_coqtop coqtop
 	  ((Minilib.canonical_path_name (Filename.dirname file),
diff --git a/ide/ideproof.ml b/ide/ideproof.ml
index 742ffc46a1..61b9f73621 100644
--- a/ide/ideproof.ml
+++ b/ide/ideproof.ml
@@ -34,7 +34,7 @@ let hook_tag_cb tag menu_content sel_cb hover_cb =
                      hover_cb start stop; false
                  | _ -> false))
 
-let mode_tactic sel_cb (proof:GText.view) = function
+let mode_tactic sel_cb (proof:GText.view) goals hints = match goals with
   | [] -> assert false
   | { Ide_intf.goal_hyp = hyps; Ide_intf.goal_ccl = cur_goal; } :: rem_goals ->
       let on_hover sel_start sel_stop =
@@ -49,35 +49,48 @@ let mode_tactic sel_cb (proof:GText.view) = function
         proof#buffer#apply_tag ~start:sel_start ~stop:sel_stop Tags.Proof.highlight
       in
       let goals_cnt = List.length rem_goals + 1 in
-      let head_str = Printf.sprintf "%d subgoal%s\n" goals_cnt (if 1 < goals_cnt then "" else "s") in
-      (* FIXME : add menu entries *)
-      let insert_hyp h =
-        let menu = [] in
-        let tags = if menu <> [] then
+      let head_str = Printf.sprintf
+        "%d subgoal%s\n" goals_cnt (if 1 < goals_cnt then "" else "s")
+      in
+      let goal_str index total = Printf.sprintf
+        "\n______________________________________(%d/%d)\n" index total
+      in
+      (* Insert current goal and its hypotheses *)
+      let hyps_hints, goal_hints = match hints with
+      | None -> [], []
+      | Some (hl, h) -> (hl, h)
+      in
+      let rec insert_hyp hints hs = match hs with
+      | [] -> ()
+      | hyp :: hs ->
+        let tags, rem_hints = match hints with
+        | [] -> [], []
+        | hint :: hints ->
           let tag = proof#buffer#create_tag [] in
-          hook_tag_cb tag menu sel_cb on_hover;
-          [tag]
-          else []
+          let () = hook_tag_cb tag hint sel_cb on_hover in
+          [tag], hints
         in
-        proof#buffer#insert ~tags (h^"\n")
+        let () = proof#buffer#insert ~tags (hyp ^ "\n") in
+        insert_hyp rem_hints hs
       in
-      let insert_goal g menu index total =
-        let tags = if menu <> [] then
+      let () = proof#buffer#insert head_str in
+      let () = insert_hyp hyps_hints hyps in
+      let () =
+        let tags = if goal_hints <> [] then
           let tag = proof#buffer#create_tag [] in
-          hook_tag_cb tag menu sel_cb on_hover;
+          let () = hook_tag_cb tag goal_hints sel_cb on_hover in
           [tag]
           else []
         in
-        proof#buffer#insert (Printf.sprintf
-                               "\n______________________________________(%d/%d)\n" index total);
-        proof#buffer#insert ~tags (g^"\n")
+        proof#buffer#insert (goal_str 1 goals_cnt);
+        proof#buffer#insert ~tags (cur_goal ^ "\n")
+      in
+      (* Insert remaining goals (no hypotheses) *)
+      let fold_goal i _ { Ide_intf.goal_ccl = g } =
+        proof#buffer#insert (goal_str i goals_cnt);
+        proof#buffer#insert (g ^ "\n")
       in
-      proof#buffer#insert head_str;
-      List.iter insert_hyp hyps;
-      (* FIXME : add menu entries *)
-      insert_goal cur_goal [] 1 goals_cnt;
-      let fold_goal i _ { Ide_intf.goal_ccl = g } = insert_goal g [] i goals_cnt in
-      Minilib.list_fold_left_i fold_goal 2 () rem_goals;
+      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)
@@ -94,7 +107,7 @@ let mode_cesar (proof:GText.view) = function
       proof#buffer#insert ("thesis := \n "^cur_goal^"\n");
       ignore (proof#scroll_to_iter (proof#buffer#get_iter_at_mark `INSERT))
 
-let display mode (view:GText.view) goals =
+let display mode (view:GText.view) goals hints =
   view#buffer#set_text "";
   match goals with
     | Ide_intf.No_current_proof -> ()
@@ -115,4 +128,4 @@ let display mode (view:GText.view) goals =
       in
       List.iter iter el
     | Ide_intf.Goals g ->
-      mode view g
+      mode view g hints