aboutsummaryrefslogtreecommitdiff
path: root/lib/unicode.mli
diff options
context:
space:
mode:
authorPierre-Marie Pédrot2016-03-03 18:59:51 +0100
committerPierre-Marie Pédrot2016-03-03 19:33:49 +0100
commit508d5a99101097948b6de342295eec0d5c8cbe72 (patch)
tree6287f344756f10dc67b1c36182480a0b76ad3c4f /lib/unicode.mli
parentdb2c6f0054d3e05f82da7494ce790c04b1976401 (diff)
Fixing bug #4105: poor escaping in the protocol between CoqIDE and coqtop.
Printing invalid UTF-8 string startled GTK too much, leading to CoqIDE dying improperly. We now check that all strings outputed by Coq are proper UTF-8. This is not perfect, as CoqIDE will sometimes truncate strings which contains the null character, but at least it should not crash.
Diffstat (limited to 'lib/unicode.mli')
-rw-r--r--lib/unicode.mli3
1 files changed, 3 insertions, 0 deletions
diff --git a/lib/unicode.mli b/lib/unicode.mli
index 520203d435..65e75a20d6 100644
--- a/lib/unicode.mli
+++ b/lib/unicode.mli
@@ -26,3 +26,6 @@ val lowercase_first_char : string -> string
(** For extraction, turn a unicode string into an ascii-only one *)
val is_basic_ascii : string -> bool
val ascii_of_ident : string -> string
+
+(** Validate an UTF-8 string *)
+val is_utf8 : string -> bool