Porting Hendrik's 8.3 patch for proof tree visualization under proof

general to trunk (only printing of goal ID done - printing of
instantiated dependent evars not done).
(joint work with Arnaud)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14423 85f007b7-540e-0410-9357-904b9bb8a0f7

3 files changed, 18 insertions, 5 deletions

diff --git a/parsing/printer.ml b/parsing/printer.ml
index e8361303d6..046d55ae3c 100644
--- a/parsing/printer.ml
+++ b/parsing/printer.ml
@@ -268,13 +268,19 @@ let default_pr_goal gs =
 		       str "============================" ++ fnl ()  ++
 		       thesis ++ str " " ++  pc) ++ fnl ()
 
+(* display a goal tag *)
+let pr_goal_tag g =
+  let s = " (ID " ^ Goal.uid g ^ ")" in
+  str (emacs_str s)
+
 (* display the conclusion of a goal *)
 let pr_concl n sigma g =
   let (g,sigma) = Goal.V82.nf_evar sigma g in
   let env = Goal.V82.env sigma g in
   let pc = pr_ltype_env_at_top env (Goal.V82.concl sigma g) in
     str (emacs_str "")  ++
-      str "subgoal " ++ int n ++ str " is:" ++ cut () ++ str" "  ++ pc
+      str "subgoal " ++ int n ++ pr_goal_tag g ++
+      str " is:" ++ cut () ++ str" "  ++ pc
 
 (* display evar type: a context and a type *)
 let pr_evgl_sign gl =
@@ -304,7 +310,8 @@ let default_pr_subgoal n sigma =
     | g::rest ->
        	if p = 1 then
           let pg = default_pr_goal { sigma=sigma ; it=g } in
-          v 0 (str "subgoal " ++ int n ++ str " is:" ++ cut () ++ pg)
+          v 0 (str "subgoal " ++ int n ++ pr_goal_tag g
+	       ++ str " is:" ++ cut () ++ pg)
        	else
 	  prrec (p-1) rest
   in
@@ -329,7 +336,7 @@ let default_pr_subgoals close_cmd sigma = function
       end
   | [g] ->
       let pg = default_pr_goal { it = g ; sigma = sigma } in
-      v 0 (str ("1 "^"subgoal") ++cut () ++ pg)
+      v 0 (str ("1 "^"subgoal") ++ pr_goal_tag g ++ cut () ++ pg)
   | g1::rest ->
       let rec pr_rec n = function
         | [] -> (mt ())
@@ -340,10 +347,10 @@ let default_pr_subgoals close_cmd sigma = function
       in
       let pg1 = default_pr_goal { it = g1 ; sigma = sigma } in
       let prest = pr_rec 2 rest in
-      v 0 (int(List.length rest+1) ++ str" subgoals" ++ cut ()
+      v 0 (int(List.length rest+1) ++ str" subgoals" ++
+             str (emacs_str ", subgoal 1") ++ pr_goal_tag g1 ++ cut ()
 	   ++ pg1 ++ prest ++ fnl ())
 
-
 (**********************************************************************)
 (* Abstraction layer                                                  *)
 
diff --git a/proofs/goal.ml b/proofs/goal.ml
index 0f10c7f84b..b2e05a5241 100644
--- a/proofs/goal.ml
+++ b/proofs/goal.ml
@@ -23,6 +23,8 @@ 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
 
 (* access primitive *)
diff --git a/proofs/goal.mli b/proofs/goal.mli
index 69b2693f7e..c36b359ed6 100644
--- a/proofs/goal.mli
+++ b/proofs/goal.mli
@@ -15,6 +15,10 @@ type goal
     sort of communication pipes. But I find it heavy. *)
 val build : Evd.evar -> goal 
 
+(* Gives a unique identifier to each goal. The identifier is
+   guaranteed to contain no space. *)
+val uid : goal -> string
+
 (* Debugging help *)
 val pr_goal : goal -> Pp.std_ppcmds