diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-05-04 08:50:27 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-05-05 17:58:16 +0200 |
| commit | 787a2c911b88bff399b37bfa8e11c0f1acecc6cd (patch) | |
| tree | dcaaf6e95686245178d1723b32a13dce54cfe408 /toplevel/vernac.ml | |
| parent | 398e64567386656f8c20b75cccff6ea4805dbd79 (diff) | |
Fix bug #3659: -time should understand multibyte encodings.
We assume Coq always outputs UTF-8 (is it really the case?) and cut strings
after 30 UTF-8 characters instead of using the standard String function.
Diffstat (limited to 'toplevel/vernac.ml')
| -rw-r--r-- | toplevel/vernac.ml | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index bfdae85d5..2a599444c 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -160,7 +160,9 @@ let pr_new_syntax po loc chan_beautify ocom = and a glimpse of the executed command *) let pp_cmd_header loc com = - let shorten s = try (String.sub s 0 30)^"..." with _ -> s in + let shorten s = + if Unicode.utf8_length s > 33 then (Unicode.utf8_sub s 0 30) ^ "..." else s + in let noblank s = for i = 0 to String.length s - 1 do match s.[i] with |