Re-add the "Show Goal" command for Prooftree in PG.

It prints a goal given its internal goal id and the Stm state id.

9 files changed, 139 insertions, 1 deletions

diff --git a/doc/sphinx/proof-engine/proof-handling.rst b/doc/sphinx/proof-engine/proof-handling.rst
index 0cff987a27..03b30d5d97 100644
--- a/doc/sphinx/proof-engine/proof-handling.rst
+++ b/doc/sphinx/proof-engine/proof-handling.rst
@@ -600,6 +600,14 @@ Requesting information
       its normalized form at the current stage of the proof, useful for
       debugging universe inconsistencies.
 
+   .. cmdv:: Show Goal @num at @num
+      :name: Show Goal
+
+      This command is only available in coqtop.  Displays a goal at a
+      proof state using the goal ID number and the proof state ID number.
+      It is primarily for use by tools such as Prooftree that need to fetch
+      goal history in this way.  Prooftree is a tool for visualizing a proof
+      as a tree that runs in Proof General.
 
 .. cmd:: Guarded
 
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. *)
 
diff --git a/printing/printer.mli b/printing/printer.mli
index 4923e9ec0e..a72f319636 100644
--- a/printing/printer.mli
+++ b/printing/printer.mli
@@ -206,4 +206,4 @@ module ContextObjectMap : CMap.ExtS
 val pr_assumptionset : env -> evar_map -> types ContextObjectMap.t -> Pp.t
 
 val pr_goal_by_id : proof:Proof.t -> Id.t -> Pp.t
-
+val pr_goal_emacs : proof:Proof.t option -> int -> int -> Pp.t
diff --git a/stm/stm.ml b/stm/stm.ml
index 28d5447c44..0216eef75f 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -1105,6 +1105,7 @@ module Backtrack : sig
   (* Returns the state that the command should backtract to *)
   val undo_vernac_classifier : vernac_control -> doc:doc -> Stateid.t
   val get_prev_proof : doc:doc -> Stateid.t -> Proof.t option
+  val get_proof : doc:doc -> Stateid.t -> Proof.t option
 
 end = struct (* {{{ *)
 
@@ -1250,6 +1251,7 @@ end = struct (* {{{ *)
 end (* }}} *)
 
 let get_prev_proof = Backtrack.get_prev_proof
+let get_proof = Backtrack.get_proof
 
 let hints = ref Aux_file.empty_aux_file
 let set_compilation_hints file =
diff --git a/stm/stm.mli b/stm/stm.mli
index f1bef2dc4d..92a782d965 100644
--- a/stm/stm.mli
+++ b/stm/stm.mli
@@ -119,6 +119,8 @@ the specified state AND that has differences in the underlying proof (i.e.,
 ignoring proofview-only changes).  Used to compute proof diffs. *)
 val get_prev_proof : doc:doc -> Stateid.t -> Proof.t option
 
+val get_proof : doc:doc -> Stateid.t -> Proof.t option
+
 (* [query at ?report_with cmd] Executes [cmd] at a given state [at],
    throwing away side effects except messages. Feedback will
    be sent with [report_with], which defaults to the dummy state id *)
diff --git a/test-suite/output-coqtop/ShowGoal.out b/test-suite/output-coqtop/ShowGoal.out
new file mode 100644
index 0000000000..2eadd22db8
--- /dev/null
+++ b/test-suite/output-coqtop/ShowGoal.out
@@ -0,0 +1,73 @@
+

+Coq < 1 subgoal

+  

+  ============================

+  forall i : nat, exists j k : nat, i = j /\ j = k /\ i = k

+

+x < 

+x < 1 focused subgoal

+(shelved: 1)

+  

+  i : nat

+  ============================

+  exists k : nat, i = ?j /\ ?j = k /\ i = k

+

+x < 1 focused subgoal

+(shelved: 2)

+  

+  i : nat

+  ============================

+  i = ?j /\ ?j = ?k /\ i = ?k

+

+x < 2 focused subgoals

+(shelved: 2)

+  

+  i : nat

+  ============================

+  i = ?j

+

+subgoal 2 is:

+ ?j = ?k /\ i = ?k

+

+x < 1 focused subgoal

+(shelved: 1)

+  

+  i : nat

+  ============================

+  i = ?k /\ i = ?k

+

+x < 2 focused subgoals

+(shelved: 1)

+  

+  i : nat

+  ============================

+  i = ?k

+

+subgoal 2 is:

+ i = ?k

+

+x < 1 subgoal

+  

+  i : nat

+  ============================

+  i = i

+

+x < goal ID 16 at state 5

+  

+  i : nat

+  ============================

+  i = ?j /\ ?j = ?k /\ i = ?k

+

+x < goal ID 16 at state 7

+  

+  i : nat

+  ============================

+  i = i /\ i = ?k /\ i = ?k

+

+x < goal ID 16 at state 9

+  

+  i : nat

+  ============================

+  i = i /\ i = i /\ i = i

+

+x < 

diff --git a/test-suite/output-coqtop/ShowGoal.v b/test-suite/output-coqtop/ShowGoal.v
new file mode 100644
index 0000000000..9545254770
--- /dev/null
+++ b/test-suite/output-coqtop/ShowGoal.v
@@ -0,0 +1,11 @@
+Lemma x: forall(i : nat), exists(j k : nat), i = j /\ j = k /\ i = k.
+Proof using.
+  eexists.
+  eexists.
+  split.
+    trivial.
+  split.
+    trivial.
+Show Goal 16 at 5.
+Show Goal 16 at 7.
+Show Goal 16 at 9.
diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml
index 4077c02604..4bcde566e3 100644
--- a/toplevel/coqloop.ml
+++ b/toplevel/coqloop.ml
@@ -403,6 +403,11 @@ let rec vernac_loop ~state =
       top_goal_print ~doc:state.doc c state.proof nstate.proof;
       vernac_loop ~state:nstate
 
+    | Some (VernacShowGoal {gid; sid}) ->
+      let proof = Stm.get_proof ~doc:state.doc (Stateid.of_int sid) in
+      Feedback.msg_notice (Printer.pr_goal_emacs ~proof gid sid);
+      vernac_loop ~state
+
     | None ->
       top_stderr (fnl ()); exit 0
 
diff --git a/toplevel/g_toplevel.mlg b/toplevel/g_toplevel.mlg
index cddcd5faa7..fed337ab03 100644
--- a/toplevel/g_toplevel.mlg
+++ b/toplevel/g_toplevel.mlg
@@ -11,6 +11,8 @@
 {
 open Pcoq
 open Pcoq.Prim
+open Tok
+open Util
 open Vernacexpr
 
 (* Vernaculars specific to the toplevel *)
@@ -19,6 +21,7 @@ type vernac_toplevel =
   | VernacDrop
   | VernacQuit
   | VernacControl of vernac_control
+  | VernacShowGoal of { gid : int; sid: int }
 
 module Toplevel_ : sig
   val vernac_toplevel : vernac_toplevel option Entry.t
@@ -29,6 +32,21 @@ end
 
 open Toplevel_
 
+let err () = raise Stream.Failure
+
+let test_show_goal =
+  Pcoq.Entry.of_parser "test_show_goal"
+    (fun strm ->
+      match stream_nth 0 strm with
+      | IDENT "Show" ->
+          (match stream_nth 1 strm with
+          | IDENT "Goal" ->
+            (match stream_nth 2 strm with
+              | NUMERAL _ -> ()
+              | _ -> err ())
+          | _ -> err ())
+      | _ -> err ())
+
 }
 
 GRAMMAR EXTEND Gram
@@ -38,6 +56,9 @@ GRAMMAR EXTEND Gram
       | IDENT "Quit"; "." -> { Some VernacQuit }
       | IDENT "Backtrack"; n = natural ; m = natural ; p = natural; "." ->
         { Some (VernacBacktrack (n,m,p)) }
+      (* show a goal for the specified proof state *)
+      | test_show_goal; IDENT "Show"; IDENT "Goal"; gid = natural; IDENT "at"; sid = natural; "." ->
+          { Some (VernacShowGoal {gid; sid}) }
       | cmd = Pvernac.Vernac_.main_entry ->
               { match cmd with
               | None -> None