diff options
| author |  aspiwack <aspiwack@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-09-12 10:04:25 +0000 |
|---|---|---|
| committer | aspiwack <aspiwack@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-09-12 10:04:25 +0000 |
| commit | 03b99149b5ab569be43d6cb3d34fb4766931074d (patch) | |
| tree | 7a99e224c95c8e4b40372bdcf6880a11ece24799 /parsing | |
| parent | 0c0481a2fdea2e5efb30d9cd11563e04c2861077 (diff) | |
Adds a new command Show Goal (e.g. Show Goal "42") printing a goal using the uid returned by Goal.uid.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14467 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/g_proofs.ml4 | 6 | ||||
| -rw-r--r-- | parsing/ppvernac.ml | 6 | ||||
| -rw-r--r-- | parsing/printer.ml | 7 | ||||
| -rw-r--r-- | parsing/printer.mli | 1 |
4 files changed, 17 insertions, 3 deletions
diff --git a/parsing/g_proofs.ml4 b/parsing/g_proofs.ml4 index 3139f5759..0f5d80a83 100644 --- a/parsing/g_proofs.ml4 +++ b/parsing/g_proofs.ml4 @@ -66,8 +66,10 @@ GEXTEND Gram | IDENT "BeginSubproof" -> VernacSubproof None | IDENT "BeginSubproof"; n = natural -> VernacSubproof (Some n) | IDENT "EndSubproof" -> VernacEndSubproof - | IDENT "Show" -> VernacShow (ShowGoal None) - | IDENT "Show"; n = natural -> VernacShow (ShowGoal (Some n)) + | IDENT "Show" -> VernacShow (ShowGoal OpenSubgoals) + | IDENT "Show"; n = natural -> VernacShow (ShowGoal (NthGoal n)) + | IDENT "Show"; IDENT "Goal"; n = string -> + VernacShow (ShowGoal (GoalId n)) | IDENT "Show"; IDENT "Implicit"; IDENT "Arguments"; n = OPT natural -> VernacShow (ShowGoalImplicitly n) | IDENT "Show"; IDENT "Node" -> VernacShow ShowNode diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml index 375e071f8..bb20dc7fc 100644 --- a/parsing/ppvernac.ml +++ b/parsing/ppvernac.ml @@ -466,8 +466,12 @@ let rec pr_vernac = function str "Backtrack" ++ spc() ++ prlist_with_sep sep int [i;j;k] | VernacFocus i -> str"Focus" ++ pr_opt int i | VernacShow s -> + let pr_goal_reference = function + | OpenSubgoals -> mt () + | NthGoal n -> spc () ++ int n + | GoalId n -> spc () ++ str n in let pr_showable = function - | ShowGoal n -> str"Show" ++ pr_opt int n + | ShowGoal n -> str"Show" ++ pr_goal_reference n | ShowGoalImplicitly n -> str"Show Implicit Arguments" ++ pr_opt int n | ShowProof -> str"Show Proof" | ShowNode -> str"Show Node" diff --git a/parsing/printer.ml b/parsing/printer.ml index 046d55ae3..232551984 100644 --- a/parsing/printer.ml +++ b/parsing/printer.ml @@ -403,6 +403,13 @@ let pr_nth_open_subgoal n = let { it=gls ; sigma=sigma } = Proof.V82.subgoals pf in pr_subgoal n sigma gls +let pr_goal_by_id id = + let p = Proof_global.give_me_the_proof () in + let g = Goal.get_by_uid id in + try + Proof.in_proof p (fun sigma -> pr_goal {it=g;sigma=sigma}) + with Not_found -> error "Invalid goal identifier." + (* Elementary tactics *) let pr_prim_rule = function diff --git a/parsing/printer.mli b/parsing/printer.mli index cdd2f4277..b7e581cd5 100644 --- a/parsing/printer.mli +++ b/parsing/printer.mli @@ -136,6 +136,7 @@ val prterm : constr -> std_ppcmds (** = pr_lconstr *) It is used primarily by the Print Assumption command. *) val pr_assumptionset : env -> Term.types Environ.ContextObjectMap.t ->std_ppcmds +val pr_goal_by_id : string -> std_ppcmds type printer_pr = { pr_subgoals : string option -> evar_map -> goal list -> std_ppcmds; |