diff options
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 |