Merge branch 'master' into ltac2-hooks

5 files changed, 35 insertions, 12 deletions

diff --git a/ide/coq.ml b/ide/coq.ml
index 3a1d877872..cd45e2fcdc 100644
--- a/ide/coq.ml
+++ b/ide/coq.ml
@@ -519,6 +519,7 @@ struct
   let all_basic = ["Printing"; "All"]
   let existential = ["Printing"; "Existential"; "Instances"]
   let universes = ["Printing"; "Universes"]
+  let unfocused = ["Printing"; "Unfocused"]
 
   type bool_descr = { opts : t list; init : bool; label : string }
 
@@ -534,7 +535,8 @@ struct
       label = "Display _existential variable instances" };
     { opts = [universes]; init = false; label = "Display _universe levels" };
     { opts = [all_basic;existential;universes]; init = false;
-      label = "Display all _low-level contents" }
+      label = "Display all _low-level contents" };
+    { opts = [unfocused]; init = false; label = "Display _unfocused goals" }
   ]
 
   (** The current status of the boolean options *)
@@ -549,6 +551,8 @@ struct
 
   let _ = reset ()
 
+  let printing_unfocused () = Hashtbl.find current_state unfocused
+
   (** Transmitting options to coqtop *)
 
   let enforce h k =
diff --git a/ide/coq.mli b/ide/coq.mli
index ab8c12a6f1..e8e2f5239e 100644
--- a/ide/coq.mli
+++ b/ide/coq.mli
@@ -140,6 +140,8 @@ sig
 
   val set : t -> bool -> unit
 
+  val printing_unfocused: unit -> bool
+
   (** [enforce] transmits to coq the current option values.
       It is also called by [goals] and [evars] above. *)
 
diff --git a/ide/coqide_ui.ml b/ide/coqide_ui.ml
index 91c281c8d8..717c4000f5 100644
--- a/ide/coqide_ui.ml
+++ b/ide/coqide_ui.ml
@@ -85,6 +85,7 @@ let init () =
 \n    <menuitem action='Display existential variable instances' />\
 \n    <menuitem action='Display universe levels' />\
 \n    <menuitem action='Display all low-level contents' />\
+\n    <menuitem action='Display unfocused goals' />\
 \n  </menu>\
 \n  <menu action='Navigation'>\
 \n    <menuitem action='Forward' />\
diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml
index 966a94da91..56ada9d132 100644
--- a/ide/ide_slave.ml
+++ b/ide/ide_slave.ml
@@ -54,7 +54,8 @@ let coqide_known_option table = List.mem table [
   ["Printing";"All"];
   ["Printing";"Records"];
   ["Printing";"Existential";"Instances"];
-  ["Printing";"Universes"]]
+  ["Printing";"Universes"];
+  ["Printing";"Unfocused"]]
 
 let is_known_option cmd = match cmd with
   | VernacSetOption (o,BoolValue true)
diff --git a/ide/wg_ProofView.ml b/ide/wg_ProofView.ml
index f801091cfc..0bf5afbfdb 100644
--- a/ide/wg_ProofView.ml
+++ b/ide/wg_ProofView.ml
@@ -47,7 +47,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_skel) goals hints = match goals with
+let mode_tactic sel_cb (proof : #GText.view_skel) goals ~unfoc_goals hints = match goals with
   | [] -> assert false
   | { Interface.goal_hyp = hyps; Interface.goal_ccl = cur_goal; } :: rem_goals ->
       let on_hover sel_start sel_stop =
@@ -65,8 +65,11 @@ let mode_tactic sel_cb (proof : #GText.view_skel) goals hints = match goals with
       let head_str = Printf.sprintf
         "%d subgoal%s\n" goals_cnt (if 1 < goals_cnt then "s" else "")
       in
-      let goal_str index total = Printf.sprintf
-        "______________________________________(%d/%d)\n" index total
+      let goal_str ?(shownum=false) index total =
+        if shownum then Printf.sprintf
+                          "______________________________________(%d/%d)\n" index total
+        else Printf.sprintf
+               "______________________________________\n"
       in
       (* Insert current goal and its hypotheses *)
       let hyps_hints, goal_hints = match hints with
@@ -97,18 +100,29 @@ let mode_tactic sel_cb (proof : #GText.view_skel) goals hints = match goals with
           [tag]
           else []
         in
-        proof#buffer#insert (goal_str 1 goals_cnt);
+        proof#buffer#insert (goal_str ~shownum:true 1 goals_cnt);
         insert_xml proof#buffer (Richpp.richpp_of_pp width cur_goal);
         proof#buffer#insert "\n"
       in
       (* Insert remaining goals (no hypotheses) *)
-      let fold_goal i _ { Interface.goal_ccl = g } =
-        proof#buffer#insert (goal_str i goals_cnt);
+      let fold_goal ?(shownum=false) i _ { Interface.goal_ccl = g } =
+        proof#buffer#insert (goal_str ~shownum i goals_cnt);
         insert_xml proof#buffer (Richpp.richpp_of_pp width g);
         proof#buffer#insert "\n"
       in
-      let () = Util.List.fold_left_i fold_goal 2 () rem_goals in
-
+      let () = Util.List.fold_left_i (fold_goal ~shownum:true) 2 () rem_goals in
+      (* show unfocused goal if option set *)
+      (* Insert remaining goals (no hypotheses) *)
+      if Coq.PrintOpt.printing_unfocused () then
+        begin
+          ignore(proof#buffer#place_cursor ~where:(proof#buffer#end_iter));
+          let unfoc = List.flatten (List.rev (List.map (fun (x,y) -> x@y) unfoc_goals)) in
+          if unfoc<>[] then
+            begin
+              proof#buffer#insert "\nUnfocused Goals:\n";
+              Util.List.fold_left_i (fold_goal ~shownum:false) 0 () unfoc
+            end
+        end;
       ignore(proof#buffer#place_cursor
                ~where:(proof#buffer#end_iter#backward_to_tag_toggle
                          (Some Tags.Proof.goal)));
@@ -172,8 +186,9 @@ let display mode (view : #GText.view_skel) goals hints evars =
       in
       List.iteri iter bg
     end
-  | Some { Interface.fg_goals = fg } ->
-    mode view fg hints
+  | Some { Interface.fg_goals = fg; bg_goals = bg } ->
+    mode view fg ~unfoc_goals:bg hints
+
 
 let proof_view () =
   let buffer = GSourceView2.source_buffer