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 /printing | |
| 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 'printing')
| -rw-r--r-- | printing/printer.ml | 16 | ||||
| -rw-r--r-- | printing/printer.mli | 2 |
2 files changed, 17 insertions, 1 deletions
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 |