diff options
| author | Jim Fehrle | 2019-06-08 05:04:41 -0700 |
|---|---|---|
| committer | Jim Fehrle | 2019-06-25 12:45:03 -0700 |
| commit | 403917b7d9ecb2ddfaaac2185c355d415d5fa5bc (patch) | |
| tree | e5afcff136068558ac11b7643709be9a7710ebd5 /toplevel | |
| parent | 7dfcb0f7c817e66280ab37b6c653b5596a16c249 (diff) | |
Re-add the "Show Goal" command for Prooftree in PG.
It prints a goal given its internal goal id and the Stm state id.
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/coqloop.ml | 5 | ||||
| -rw-r--r-- | toplevel/g_toplevel.mlg | 21 |
2 files changed, 26 insertions, 0 deletions
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 |