From 180a27f8d2b7ba2d7913c37ae01c946acb8c813e Mon Sep 17 00:00:00 2001
From: gareuselesinge
Date: Fri, 8 Mar 2013 14:36:04 +0000
Subject: catch failures of pr_vernac to make -time failsafe

Printing Ltac code is broken. This was not compiling with -time

  Ltac pop_succn e := eval lazy beta iota delta [plus] in (1 + 1).

The bug in the pretty printer should be fixed too...

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16262 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 toplevel/vernac.ml | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index 2cac3d98c7..33f6a01108 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -62,7 +62,10 @@ let display_cmd_header loc com =
     s
   in
   let (start,stop) = Loc.unloc loc in
-  let cmd = noblank (shorten (string_of_ppcmds (Ppvernac.pr_vernac com)))
+  let safe_pr_vernac x =
+    try Ppvernac.pr_vernac x
+    with e -> str (Printexc.to_string e) in
+  let cmd = noblank (shorten (string_of_ppcmds (safe_pr_vernac com)))
   in
   Pp.pp (str "Chars " ++ int start ++ str " - " ++ int stop ++
 	 str (" ["^cmd^"] "));
-- 
cgit v1.2.3