From 5a21a70dd1a5be9a7de01bf1eeae630395a3dce4 Mon Sep 17 00:00:00 2001
From: vgross
Date: Thu, 14 Jan 2010 18:06:32 +0000
Subject: Fix uncaught exception

On windows platform, exceptions are not always encoded in utf-8, thus
failing the assert.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12675 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 ide/coqide.ml | 31 +++++++++++++++++--------------
 1 file changed, 17 insertions(+), 14 deletions(-)

diff --git a/ide/coqide.ml b/ide/coqide.ml
index 6e3d867870..542ebe502a 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -926,23 +926,26 @@ object(self)
       self#insert_message (if show_output then msg else "") in
     let display_error e =
       let (s,loc) = Coq.process_exn e in
-        assert (Glib.Utf8.validate s);
-        self#insert_message s;
-        message_view#misc#draw None;
-        if localize then
-          (match Option.map Util.unloc loc with
-             | None -> ()
-             | Some (start,stop) ->
-                 let convert_pos = byte_offset_to_char_offset phrase in
-                 let start = convert_pos start in
-                 let stop = convert_pos stop in
-                 let i = self#get_start_of_input in
-                 let starti = i#forward_chars start in
-                 let stopi = i#forward_chars stop in
+        if not (Glib.Utf8.validate s) then
+          flash_info "This error is so nasty that I can't even display it." 
+        else begin
+          self#insert_message s;
+          message_view#misc#draw None;
+          if localize then
+            (match Option.map Util.unloc loc with
+               | None -> ()
+               | Some (start,stop) ->
+                   let convert_pos = byte_offset_to_char_offset phrase in
+                   let start = convert_pos start in
+                   let stop = convert_pos stop in
+                   let i = self#get_start_of_input in
+                   let starti = i#forward_chars start in
+                   let stopi = i#forward_chars stop in
                    input_buffer#apply_tag Tags.Script.error
                      ~start:starti
                      ~stop:stopi;
-                   input_buffer#place_cursor starti) in
+                   input_buffer#place_cursor starti)
+        end in
       try
         full_goal_done <- false;
         prerr_endline "Send_to_coq starting now";
-- 
cgit v1.2.3