branchement extraction en standard (pas de Require)

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

1 files changed, 10 insertions, 6 deletions

diff --git a/toplevel/toplevel.ml b/toplevel/toplevel.ml
index 52f3a7935..124f9e9f1 100644
--- a/toplevel/toplevel.ml
+++ b/toplevel/toplevel.ml
@@ -165,15 +165,19 @@ let valid_loc dloc (b,e) =
 	  
 let valid_buffer_loc ib dloc (b,e) =
   valid_loc dloc (b,e) & b-ib.start >= 0 & e-ib.start < ib.len & b<=e 
-    
+
+(*s The Coq prompt is the name of the focused proof, if any, and "Coq"
+    otherwise. We trap all exceptions to prevent the error message printing
+    from cycling. *)
+let make_prompt () =
+  try
+    (Names.string_of_id (Pfedit.get_current_proof_name ())) ^ " < "
+  with _ -> 
+    "Coq < "
+
 (* A buffer to store the current command read on stdin. It is
  * initialized when a vernac command is immediately followed by "\n",
  * or after a Drop. *)
-let make_prompt () =
-  if Pfedit.refining () then
-    (Names.string_of_id (Pfedit.get_current_proof_name ()))^" < "
-  else "Coq < "
-
 let top_buffer =
   let pr() = (make_prompt())^(emacs_str (String.make 1 (Char.chr 249)))
   in