Adapting the IDE interface with the focussed display.

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

1 files changed, 8 insertions, 6 deletions

diff --git a/toplevel/ide_slave.ml b/toplevel/ide_slave.ml
index 2b5d4b5a5d..4537dc405d 100644
--- a/toplevel/ide_slave.ml
+++ b/toplevel/ide_slave.ml
@@ -178,19 +178,21 @@ let process_goal sigma g =
   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)) :: 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
   { Interface.goal_hyp = hyps; Interface.goal_ccl = ccl; Interface.goal_id = id; }
-(*         hyps,(ccl,concl_next_tac sigma g)) *)
 
 let goals () =
   try
     let pfts = Proof_global.give_me_the_proof () in
-    let { Evd.it = all_goals ; sigma = sigma } = Proof.V82.subgoals pfts in
-    let fg = List.map (process_goal sigma) all_goals in
-    let { Evd.it = bgoals ; sigma = sigma } = Proof.V82.background_subgoals pfts in
-    let bg = List.map (process_goal sigma) bgoals in
+    let (goals, zipper, sigma) = Proof.proof pfts in
+    let fg = List.map (process_goal sigma) goals in
+    let map_zip (lg, rg) =
+      let lg = List.map (process_goal sigma) lg in
+      let rg = List.map (process_goal sigma) rg in
+      (lg, rg)
+    in
+    let bg = List.map map_zip zipper in
     Some { Interface.fg_goals = fg; Interface.bg_goals = bg; }
   with Proof_global.NoCurrentProof -> None