Adding a printer for Proof.proof reflecting the focusing layout.

This is a modest contribution serving before all the purpose of
displaying the focus stack and the shelf and give_up list. It does not
print the sigma (while it could).

Any improvements are welcome.

2 files changed, 18 insertions, 0 deletions

diff --git a/proofs/proof.ml b/proofs/proof.ml
index 0a3b08c04a..b2103489a7 100644
--- a/proofs/proof.ml
+++ b/proofs/proof.ml
@@ -372,6 +372,22 @@ let in_proof p k = k (Proofview.return p.proofview)
 let unshelve p =
   { p with proofview = Proofview.unshelve (p.shelf) (p.proofview) ; shelf = [] }
 
+let pr_proof p =
+  let p = map_structured_proof p (fun _sigma g -> g) in
+  Pp.(
+    let pr_goal_list = prlist_with_sep spc Goal.pr_goal in
+    let rec aux acc = function
+      | [] -> acc
+      | (before,after)::stack ->
+         aux (pr_goal_list before ++ spc () ++ str "{" ++ acc ++ str "}" ++ spc () ++
+              pr_goal_list after) stack in
+    str "[" ++ str "focus structure: " ++
+               aux (pr_goal_list p.fg_goals) p.bg_goals ++ str ";" ++ spc () ++
+    str "shelved: " ++ pr_goal_list p.shelved_goals ++ str ";" ++ spc () ++
+    str "given up: " ++ pr_goal_list p.given_up_goals ++
+    str "]"
+  )
+
 (*** Compatibility layer with <=v8.2 ***)
 module V82 = struct
   let subgoals p =
diff --git a/proofs/proof.mli b/proofs/proof.mli
index 5053fc7fb9..8dc165e72e 100644
--- a/proofs/proof.mli
+++ b/proofs/proof.mli
@@ -182,6 +182,8 @@ val in_proof : proof -> (Evd.evar_map -> 'a) -> 'a
    focused goals. *)
 val unshelve : proof -> proof
 
+val pr_proof : proof -> Pp.std_ppcmds
+
 (*** Compatibility layer with <=v8.2 ***)
 module V82 : sig
   val subgoals : proof -> Goal.goal list Evd.sigma