Replaced goal api call with a proper structure. This disables menu hints in CoqIDE (* FIXME *)

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

4 files changed, 50 insertions, 22 deletions

diff --git a/ide/ideproof.ml b/ide/ideproof.ml
index 783ade6048..58e7d2734b 100644
--- a/ide/ideproof.ml
+++ b/ide/ideproof.ml
@@ -36,7 +36,7 @@ let hook_tag_cb tag menu_content sel_cb hover_cb =
 
 let mode_tactic sel_cb (proof:GText.view) = function
   | [] -> assert false
-  | (hyps,(cur_goal,cur_goal_menu))::rem_goals ->
+  | { Ide_intf.goal_hyp = hyps; Ide_intf.goal_ccl = cur_goal; } :: rem_goals ->
       let on_hover sel_start sel_stop =
         proof#buffer#remove_tag
           ~start:proof#buffer#start_iter
@@ -50,10 +50,16 @@ let mode_tactic sel_cb (proof:GText.view) = function
       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
-      let insert_hyp (h,menu) =
-        let tag = proof#buffer#create_tag [] in
-        hook_tag_cb tag menu sel_cb on_hover;
-        proof#buffer#insert ~tags:[tag] (h^"\n")
+      (* FIXME : add menu entries *)
+      let insert_hyp h =
+        let menu = [] in
+        let tags = if menu <> [] then
+          let tag = proof#buffer#create_tag [] in
+          hook_tag_cb tag menu sel_cb on_hover;
+          [tag]
+          else []
+        in
+        proof#buffer#insert ~tags (h^"\n")
       in
       let insert_goal g menu index total =
         let tags = if menu <> [] then
@@ -68,8 +74,10 @@ let mode_tactic sel_cb (proof:GText.view) = function
       in
       proof#buffer#insert head_str;
       List.iter insert_hyp hyps;
-      insert_goal cur_goal cur_goal_menu 1 goals_cnt;
-      Minilib.list_fold_left_i (fun i _ (_,(g,_)) -> insert_goal g [] i goals_cnt) 2 () rem_goals;
+      (* 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;
       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)
@@ -77,10 +85,10 @@ let mode_tactic sel_cb (proof:GText.view) = function
 
 let mode_cesar (proof:GText.view) = function
   | [] -> assert false
-  | (hyps,(cur_goal,cur_goal_menu))::_ ->
+  | { Ide_intf.goal_hyp = hyps; Ide_intf.goal_ccl = cur_goal; } :: _ ->
       proof#buffer#insert "    *** Declarative Mode ***\n";
       List.iter
-        (fun (hyp,_) -> proof#buffer#insert (hyp^"\n"))
+        (fun hyp -> proof#buffer#insert (hyp^"\n"))
         hyps;
       proof#buffer#insert "______________________________________\n";
       proof#buffer#insert ("thesis := \n "^cur_goal^"\n");
diff --git a/toplevel/ide_intf.ml b/toplevel/ide_intf.ml
index 2d5b14df2b..6abea2ad83 100644
--- a/toplevel/ide_intf.ml
+++ b/toplevel/ide_intf.ml
@@ -14,9 +14,14 @@ type xml = Xml_parser.xml
 
 type 'a menu = 'a * (string * string) list
 
+type goal = {
+  goal_hyp : string list;
+  goal_ccl : string;
+}
+
 type goals =
   | Message of string
-  | Goals of ((string menu) list * string menu) list
+  | Goals of goal list
 
 (** We use phantom types and GADT to protect ourselves against wild casts *)
 
@@ -192,20 +197,30 @@ let to_pair f g = function
 | Element ("pair", [], [x; y]) -> (f x, g y)
 | _ -> raise Marshal_error
 
+let of_goal g =
+  let hyp = of_list of_string g.goal_hyp in
+  let ccl = of_string g.goal_ccl in
+  Element ("goal", [], [hyp; ccl])
+
+let to_goal = function
+| Element ("goal", [], [hyp; ccl]) ->
+  let hyp = to_list to_string hyp in
+  let ccl = to_string ccl in
+  { goal_hyp = hyp; goal_ccl = ccl }
+| _ -> raise Marshal_error
+
 let of_goals = function
 | Message s ->
   Element ("goals", ["val", "message"], [PCData s])
 | Goals l ->
-  let of_string_menu = of_pair of_string (of_list (of_pair of_string of_string)) in
-  let xml = of_list (of_pair (of_list of_string_menu) of_string_menu) l in
+  let xml = of_list of_goal l in
   Element ("goals", ["val", "goals"], [xml])
 
 let to_goals = function
 | Element ("goals", ["val", "message"], l) -> Message (raw_string l)
 | Element ("goals", ["val", "goals"], [xml]) ->
-  let to_string_menu = to_pair to_string (to_list (to_pair to_string to_string)) in
-  let ans = to_list (to_pair (to_list to_string_menu) to_string_menu) xml in
-  Goals ans
+  let l = to_list to_goal xml in
+  Goals l
 | _ -> raise Marshal_error
 
 let of_answer (q : 'a call) (r : 'a value) =
@@ -263,8 +278,8 @@ let pr_mkcases l =
 let pr_goals = function
 | Message s -> "Message: " ^ s
 | Goals gl ->
-  let pr_menu (s, _) = s in
-  let pr_goal (hyps, goal) =
+  let pr_menu s = s in
+  let pr_goal { goal_hyp = hyps; goal_ccl = goal } =
     "[" ^ String.concat "; " (List.map pr_menu hyps) ^ " |- " ^ pr_menu goal ^ "]"
   in
   String.concat " " (List.map pr_goal gl)
diff --git a/toplevel/ide_intf.mli b/toplevel/ide_intf.mli
index 9cb615265c..02b8525347 100644
--- a/toplevel/ide_intf.mli
+++ b/toplevel/ide_intf.mli
@@ -10,11 +10,14 @@
 
 type xml = Xml_parser.xml
 
-type 'a menu = 'a * (string * string) list
+type goal = {
+  goal_hyp : string list;
+  goal_ccl : string;
+}
 
 type goals =
   | Message of string
-  | Goals of ((string menu) list * string menu) list
+  | Goals of goal list
 
 type 'a call
 
diff --git a/toplevel/ide_slave.ml b/toplevel/ide_slave.ml
index 5309a45052..95a6dcf6ac 100644
--- a/toplevel/ide_slave.ml
+++ b/toplevel/ide_slave.ml
@@ -432,10 +432,12 @@ let goals () =
           string_of_ppcmds (pr_ltype_env_at_top env norm_constr) in
         let process_hyp h_env d acc =
           let d = Term.map_named_declaration (Reductionops.nf_evar sigma) d in
-          (string_of_ppcmds (pr_var_decl h_env d), hyp_next_tac sigma h_env d)::acc in
+          (string_of_ppcmds (pr_var_decl h_env d)) :: acc in
+(*           (string_of_ppcmds (pr_var_decl h_env d), hyp_next_tac sigma h_env d)::acc in *)
         let hyps =
-          List.rev (Environ.fold_named_context process_hyp env ~init:[]) in
-        (hyps,(ccl,concl_next_tac sigma g))
+          List.rev (Environ.fold_named_context process_hyp env ~init: []) in
+        { Ide_intf.goal_hyp = hyps; Ide_intf.goal_ccl = ccl }
+(*         hyps,(ccl,concl_next_tac sigma g)) *)
       in
       Ide_intf.Goals (List.map process_goal all_goals)
     end