From 9955d65b30b4285d217feb4ae6ea5076e7579bf8 Mon Sep 17 00:00:00 2001
From: monate
Date: Fri, 6 Jun 2003 13:43:32 +0000
Subject: coqide: compile sans activate repare

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4102 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 ide/coqide.ml | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/ide/coqide.ml b/ide/coqide.ml
index 7331c97861..ae7dfbec57 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -1219,11 +1219,12 @@ Please restart and report NOW.";
 	      (match t with 
 	       | VernacBeginSection _ | VernacDefineModule _ 
 	       | VernacDeclareModule _ | VernacDeclareModuleType _
-	       | VernacEndSegment _ 
+	       | VernacEndSegment _
 		 -> reset_to_mod id
 	       | _ ->  reset_to id);
 	      update_input ()
 	  | { ast = _, ( VernacStartTheoremProof _ 
+		       | VernacGoal _
 		       | VernacDefinition (_,_,ProveBody _,_,_));
 	      reset_info=Reset(id,{contents=false})} ->
 	      ignore (pop ());
@@ -2273,6 +2274,7 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S);
 	  !flash_info (f ^ " successfully compiled")
 	else begin
 	  !flash_info (f ^ " failed to compile");
+	  activate_input (notebook ())#current_page;
 	  av#process_until_end_or_error;
 	  av#insert_message "Compilation output:\n";
 	  av#insert_message res
-- 
cgit v1.2.3