From 508d5a99101097948b6de342295eec0d5c8cbe72 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 3 Mar 2016 18:59:51 +0100
Subject: 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.
---
 interp/notation.ml | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

(limited to 'interp/notation.ml')

diff --git a/interp/notation.ml b/interp/notation.ml
index 5c10e0af71..c4addbf10f 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -314,7 +314,9 @@ let declare_prim_token_interpreter sc interp (patl,uninterp,b) =
     patl
 
 let mkNumeral n = Numeral n
-let mkString s = String s
+let mkString = function
+| None -> None
+| Some s -> if Unicode.is_utf8 s then Some (String s) else None
 
 let delay dir int loc x = (dir, (fun () -> int loc x))
 
@@ -326,7 +328,7 @@ let declare_numeral_interpreter sc dir interp (patl,uninterp,inpat) =
 let declare_string_interpreter sc dir interp (patl,uninterp,inpat) =
   declare_prim_token_interpreter sc
     (fun cont loc -> function String s -> delay dir interp loc s | p -> cont loc p)
-    (patl, (fun r -> Option.map mkString (uninterp r)), inpat)
+    (patl, (fun r -> mkString (uninterp r)), inpat)
 
 let check_required_module loc sc (sp,d) =
   try let _ = Nametab.global_of_path sp in ()
-- 
cgit v1.2.3