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

4 files changed, 30 insertions, 12 deletions

diff --git a/ide/ideproof.ml b/ide/ideproof.ml
index 569e503c3b..12cb8c815a 100644
--- a/ide/ideproof.ml
+++ b/ide/ideproof.ml
@@ -130,6 +130,13 @@ let display mode (view:GText.view) goals hints evars =
   | Some { Interface.fg_goals = []; Interface.bg_goals = bg } ->
     (* No foreground proofs, but still unfocused ones *)
     view#buffer#insert "This subproof is complete, but there are still unfocused goals:\n\n";
+    let rec flatten = function
+    | [] -> []
+    | (lg, rg) :: l ->
+      let inner = flatten l in
+      List.rev_append lg inner @ rg
+    in
+    let bg = flatten (List.rev bg) in
     let iter goal =
       let msg = Printf.sprintf "%s\n" goal.Interface.goal_ccl in
       view#buffer#insert msg
diff --git a/lib/interface.mli b/lib/interface.mli
index 4c7c11ebb2..1b9c2c6389 100644
--- a/lib/interface.mli
+++ b/lib/interface.mli
@@ -44,8 +44,8 @@ type status = {
 type goals = {
   fg_goals : goal list;
   (** List of the focussed goals *)
-  bg_goals : goal list;
-  (** List of the background goals *)
+  bg_goals : (goal list * goal list) list;
+  (** Zipper representing the unfocussed background goals *)
 }
 
 type hint = (string * string) list
diff --git a/lib/serialize.ml b/lib/serialize.ml
index 1d686243fe..ed595c3146 100644
--- a/lib/serialize.ml
+++ b/lib/serialize.ml
@@ -10,7 +10,7 @@
 
 (** WARNING: TO BE UPDATED WHEN MODIFIED! *)
 
-let protocol_version = "20120511"
+let protocol_version = "20120710"
 
 (** * Interface of calls to Coq by CoqIde *)
 
@@ -384,14 +384,16 @@ let to_goal = function
 | _ -> raise Marshal_error
 
 let of_goals g =
+  let of_glist = of_list of_goal in
   let fg = of_list of_goal g.fg_goals in
-  let bg = of_list of_goal g.bg_goals in
+  let bg = of_list (of_pair of_glist of_glist) g.bg_goals in
   Element ("goals", [], [fg; bg])
 
 let to_goals = function
 | Element ("goals", [], [fg; bg]) ->
+  let to_glist = to_list to_goal in
   let fg = to_list to_goal fg in
-  let bg = to_list to_goal bg in
+  let bg = to_list (to_pair to_glist to_glist) bg in
   { fg_goals = fg; bg_goals = bg; }
 | _ -> raise Marshal_error
 
@@ -556,7 +558,14 @@ let pr_mkcases l =
 let pr_goals_aux g =
   if g.fg_goals = [] then
     if g.bg_goals = [] then "Proof completed."
-    else Printf.sprintf "Still %i unfocused goals." (List.length g.bg_goals)
+    else
+      let rec pr_focus _ = function
+      | [] -> assert false
+      | [lg, rg] -> Printf.sprintf "%i" (List.length lg + List.length rg)
+      | (lg, rg) :: l ->
+        Printf.sprintf "%i:%a" (List.length lg + List.length rg) pr_focus l
+      in
+      Printf.sprintf "Still focussed: [%a]." pr_focus g.bg_goals
   else
     let pr_menu s = s in
     let pr_goal { goal_hyp = hyps; goal_ccl = goal } =
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