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

6 files changed, 36 insertions, 1 deletions

diff --git a/proofs/goal.ml b/proofs/goal.ml
index b2e05a5241..b50177eeae 100644
--- a/proofs/goal.ml
+++ b/proofs/goal.ml
@@ -23,7 +23,6 @@ type goal = {
 (* spiwack: I don't deal with the tags, yet. It is a worthy discussion
    whether we do want some tags displayed besides the goal or not. *)
 
-let uid {content = e} = string_of_int e
 
 let pr_goal {content = e} = str "GOAL:" ++ Pp.int e
 
@@ -38,6 +37,16 @@ let build e =
     tags = []
   }
 
+
+let uid {content = e} = string_of_int e
+let get_by_uid u =
+  (* this necessarily forget about tags.
+     when tags are to be implemented, they
+     should be done another way.
+     We could use the store in evar_extra,
+     for instance. *)
+  build (int_of_string u)
+
 (* Builds a new goal with content evar [e] and 
    inheriting from goal [gl]*)
 let descendent gl e =
diff --git a/proofs/goal.mli b/proofs/goal.mli
index c36b359ed6..e9d2306594 100644
--- a/proofs/goal.mli
+++ b/proofs/goal.mli
@@ -18,6 +18,9 @@ val build : Evd.evar -> goal
 (* Gives a unique identifier to each goal. The identifier is
    guaranteed to contain no space. *)
 val uid : goal -> string
+(* Returns the goal (even if it has been partially solved)
+   corresponding to a unique identifier obtained by {!uid}. *)
+val get_by_uid : string -> goal
 
 (* Debugging help *)
 val pr_goal : goal -> Pp.std_ppcmds
diff --git a/proofs/proof.ml b/proofs/proof.ml
index 23ce2c8eb1..8283657983 100644
--- a/proofs/proof.ml
+++ b/proofs/proof.ml
@@ -410,7 +410,10 @@ let run_tactic env tac pr =
     restore_state starting_point pr;
     raise e
 
+(*** Commands ***)
 
+let in_proof p k =
+  Proofview.in_proofview p.state.proofview k
 
 
 (*** Compatibility layer with <=v8.2 ***)
diff --git a/proofs/proof.mli b/proofs/proof.mli
index 7de0a9fdfd..b4c84cbf60 100644
--- a/proofs/proof.mli
+++ b/proofs/proof.mli
@@ -154,6 +154,11 @@ val run_tactic : Environ.env -> unit Proofview.tactic -> proof -> unit
    [transaction p f] can be called on an [f] using, itself, [transaction p].*)
 val transaction : proof -> (unit -> unit) -> unit
 
+
+(*** Commands ***)
+
+val in_proof : proof -> (Evd.evar_map -> 'a) -> 'a
+
 (*** Compatibility layer with <=v8.2 ***)
 module V82 : sig
   val subgoals : proof -> Goal.goal list Evd.sigma
diff --git a/proofs/proofview.ml b/proofs/proofview.ml
index 3964692b10..b76c802dfd 100644
--- a/proofs/proofview.ml
+++ b/proofs/proofview.ml
@@ -433,6 +433,12 @@ let tclSENSITIVE s =
     fun env -> { go = fun sk fk step -> sk () fk (sensitive_on_step s env step) }
   end
 
+
+(*** Commands ***)
+
+let in_proofview p k =
+  k p.solution
+
 module Notations = struct
   let (>-) = Goal.bind
   let (>>-) = tclGOALBINDU
diff --git a/proofs/proofview.mli b/proofs/proofview.mli
index e8cf7d26df..25a58a482a 100644
--- a/proofs/proofview.mli
+++ b/proofs/proofview.mli
@@ -153,6 +153,15 @@ val tclGOALBINDU : 'a Goal.sensitive -> ('a -> unit tactic) -> unit tactic
 (* [tclSENSITIVE] views goal-type tactics as a special kind of tactics.*)
 val tclSENSITIVE : Goal.subgoals Goal.sensitive -> unit tactic 
 
+
+(*** Commands ***)
+
+val in_proofview : proofview -> (Evd.evar_map -> 'a) -> 'a
+
+
+
+
+
 (* Notations for building tactics. *)
 module Notations : sig
   (* Goal.bind *)