- 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

4 files changed, 28 insertions, 11 deletions

diff --git a/dev/ocamldebug-coq.template b/dev/ocamldebug-coq.template
index ac5ec1e0d5..31e928063d 100644
--- a/dev/ocamldebug-coq.template
+++ b/dev/ocamldebug-coq.template
@@ -26,4 +26,5 @@ exec $OCAMLDEBUG \
 	-I $COQTOP/contrib/subtac     -I $COQTOP/contrib/funind \
         -I $COQTOP/contrib/rtauto     -I $COQTOP/contrib/setoid_ring \
         -I $COQTOP/contrib/recdef     -I $COQTOP/contrib/dp \
+        -I $COQTOP/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
diff --git a/test-suite/output/Notations.out b/test-suite/output/Notations.out
index 6c69c097dd..acfcd5aff0 100644
--- a/test-suite/output/Notations.out
+++ b/test-suite/output/Notations.out
@@ -50,6 +50,8 @@ Nil
      : forall A : Type, list A
 NIL:list nat
      : list nat
+(false && I 3)%bool /\ I 6
+     : Prop
 [|1, 2, 3; 4, 5, 6|]
      : Z * Z * Z * (Z * Z * Z)
 fun f : Z -> Z -> Z -> Z => {|f; 0; 1; 2|}:Z
diff --git a/test-suite/output/Notations.v b/test-suite/output/Notations.v
index f19ba998fa..4577f0e196 100644
--- a/test-suite/output/Notations.v
+++ b/test-suite/output/Notations.v
@@ -130,6 +130,18 @@ Check Nil.
 Notation NIL := nil.
 Check NIL : list nat.
 
+
+(**********************************************************************)
+(* Test printing of notation with coercions in scope of a coercion    *)
+
+Open Scope nat_scope.
+
+Coercion is_true := fun b => b=true.
+Coercion of_nat n := match n with 0 => true | _ => false end.
+Notation "'I' x" := (of_nat (S x) || true)%bool (at level 10).
+
+Check (false && I 3)%bool /\ I 6.
+
 (**********************************************************************)
 (* Check notations with several recursive patterns                    *)