diff options
| author |  gareuselesinge <gareuselesinge@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-03-08 14:36:04 +0000 |
|---|---|---|
| committer | gareuselesinge <gareuselesinge@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-03-08 14:36:04 +0000 |
| commit | 180a27f8d2b7ba2d7913c37ae01c946acb8c813e (patch) | |
| tree | f9b205e4b38bb631b38c0bbfee717fe73d6ae605 | |
| parent | 9d0fde51068c1f1c16142865457a43d2fd5143ee (diff) | |
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
| -rw-r--r-- | toplevel/vernac.ml | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index 2cac3d98c..33f6a0110 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^"] ")); |