From 403917b7d9ecb2ddfaaac2185c355d415d5fa5bc Mon Sep 17 00:00:00 2001
From: Jim Fehrle
Date: Sat, 8 Jun 2019 05:04:41 -0700
Subject: Re-add the "Show Goal" command for Prooftree in PG. It prints a goal
 given its internal goal id and the Stm state id.

---
 printing/printer.ml | 16 ++++++++++++++++
 1 file changed, 16 insertions(+)

(limited to 'printing/printer.ml')

diff --git a/printing/printer.ml b/printing/printer.ml
index 0bcea3b01c..1f68018678 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -831,6 +831,22 @@ let pr_goal_by_id ~proof id =
       pr_selected_subgoal (pr_id id) sigma g)
   with Not_found -> user_err Pp.(str "No such goal.")
 
+(** print a goal identified by the goal id as it appears in -emacs mode.
+    sid should be the Stm state id corresponding to proof.  Used to support
+    the Prooftree tool in Proof General. (https://askra.de/software/prooftree/).
+*)
+let pr_goal_emacs ~proof gid sid =
+  match proof with
+  | None -> user_err Pp.(str "No proof for that state.")
+  | Some proof ->
+    let pr gs =
+      v 0 ((str "goal ID " ++ (int gid) ++ str " at state " ++ (int sid)) ++ cut ()
+          ++ pr_goal gs)
+    in
+    try
+      Proof.in_proof proof (fun sigma -> pr {it=(Evar.unsafe_of_int gid);sigma=sigma;})
+    with Not_found -> user_err Pp.(str "No such goal.")
+
 (* Printer function for sets of Assumptions.assumptions.
    It is used primarily by the Print Assumptions command. *)
 
-- 
cgit v1.2.3