diff options
| -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^"] ")); |