From e0003f41bd1b14b3cc74127355fe9504445750d1 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Fri, 7 Nov 2008 17:10:50 +0000
Subject: - Ajout possibilité de lancer ocamldebug sur coqide - Correction bug
 #1815 sur "coqide dir_inexistant/nom_fichier" - Tests oubliés de la révision
 11438 (amélioration affichage coercions)

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

(limited to 'ide')

diff --git a/ide/coqide.ml b/ide/coqide.ml
index 353cf304b8..3b8696e9ba 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -482,10 +482,11 @@ let input_channel b ic =
       Buffer.add_substring b buf 0 !len
     done
 
-let with_file name ~f =
-  let ic = open_in_gen [Open_rdonly;Open_creat] 0o644 name in
-    try f ic; close_in ic with exn -> 
-      close_in ic; !flash_info ("Error: "^Printexc.to_string exn)
+let with_file handler name ~f =
+  try
+    let ic = open_in_gen [Open_rdonly;Open_creat] 0o644 name in
+    try f ic; close_in ic with e -> close_in ic; raise e
+  with Sys_error s -> handler s
 
 type info =  {start:GText.mark;
 	      stop:GText.mark;
@@ -713,7 +714,7 @@ object(self)
 		try
 		  if is_active then self#reset_initial;
 		  let b = Buffer.create 1024 in
-		    with_file f ~f:(input_channel b);
+		    with_file !flash_info f ~f:(input_channel b);
 		    let s = try_convert (Buffer.contents b) in
 		      input_buffer#set_text s;
 		      self#update_stats;
@@ -1871,7 +1872,7 @@ let main files =
       let file_factory = new GMenu.factory ~accel_path:"<CoqIde MenuBar>/File/" file_menu ~accel_group in
 
       (* File/Load Menu *)
-      let load f =
+      let load_file handler f =
 	let f = absolute_filename f in		
 	  try
 	    prerr_endline "Loading file starts";
@@ -1886,7 +1887,7 @@ let main files =
 	    prerr_endline "Loading: must open";
 	    let b = Buffer.create 1024 in
 	      prerr_endline "Loading: get raw content";
-	      with_file f ~f:(input_channel b);
+	      with_file handler f ~f:(input_channel b);
 	      prerr_endline "Loading: convert content";
 	      let s = do_convert (Buffer.contents b) in
 		prerr_endline "Loading: create view";
@@ -1922,8 +1923,9 @@ let main files =
 		      prerr_endline "Loading: success"
 	  with       
 	    | Vector.Found i -> set_current_view i
-	    | e -> !flash_info ("Load failed: "^(Printexc.to_string e))
+	    | e -> handler ("Load failed: "^(Printexc.to_string e))
       in
+      let load f = load_file !flash_info f in
       let load_m = file_factory#add_item "_New" 
 	~key:GdkKeysyms._N in
       let load_f () = 	  
@@ -3632,9 +3634,9 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S);
 								begin
 								  List.iter (fun f -> 
 									       if Sys.file_exists f then load f else 
-										 if Filename.check_suffix f ".v" 
-										 then load f 
-										 else load (f^".v")) files;
+                                                                                 let f = if Filename.check_suffix f ".v" then f else f^".v" in
+										 load_file (fun s -> print_endline s; exit 1) f)
+                                                                    files;
 								  activate_input 0
 								end
 							      else
-- 
cgit v1.2.3