Imported Upstream version 8.1~gammaupstream/8.1.gamma

9 files changed, 508 insertions, 348 deletions

diff --git a/ide/command_windows.ml b/ide/command_windows.ml
index 1f40e057..768d125c 100644
--- a/ide/command_windows.ml
+++ b/ide/command_windows.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: command_windows.ml 5920 2004-07-16 20:01:26Z herbelin $ *)
+(* $Id: command_windows.ml 9189 2006-09-29 12:39:24Z notin $ *)
 
 class command_window () = 
   let window = GWindow.window 
@@ -15,7 +15,7 @@ class command_window () =
 		 ~position:`CENTER
 		 ~title:"CoqIde queries" ~show:false ()
   in
-  let accel_group = GtkData.AccelGroup.create () in
+  let _ = GtkData.AccelGroup.create () in
   let vbox = GPack.vbox ~homogeneous:false ~packing:window#add () in
   let toolbar = GButton.toolbar 
 		  ~orientation:`HORIZONTAL 
@@ -52,7 +52,7 @@ class command_window () =
       ()
   in
 
-  let kill_page_menu = 
+  let _ = 
     toolbar#insert_button
       ~tooltip:"Kill Page"
       ~text:"Kill Page"
diff --git a/ide/coq.ml b/ide/coq.ml
index 32e8a02e..fae34ef2 100644
--- a/ide/coq.ml
+++ b/ide/coq.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: coq.ml 9024 2006-07-06 10:38:15Z herbelin $ *)
+(* $Id: coq.ml 9263 2006-10-23 12:08:08Z barras $ *)
 
 open Vernac
 open Vernacexpr
@@ -19,6 +19,7 @@ open Printer
 open Environ
 open Evarutil
 open Evd
+open Decl_mode
 open Hipattern
 open Tacmach
 open Reductionops
@@ -53,43 +54,41 @@ let version () =
   let date =
     if Glib.Utf8.validate Coq_config.date
     then Coq_config.date
-    else "<date not printable>"
-  in
-  Printf.sprintf 
-    "The Coq Proof Assistant, version %s (%s)\
-   \nConfigured on %s\
-   \nArchitecture %s running %s operating system\
-   \nGtk version is %s\
-   \nThis is the %s version (%s is the best one for this architecture and OS)\
-   \n"
-    Coq_config.version date Coq_config.compile_date
-    Coq_config.arch Sys.os_type
-    (let x,y,z = GMain.Main.version in Printf.sprintf "%d.%d.%d" x y z)
+    else "<date not printable>" in
+  let get_version_date () =
+    try
+      let ch = open_in (Coq_config.coqtop^"/revision") in
+      let ver = input_line ch in
+      let rev = input_line ch in
+	(ver,rev)
+    with _ -> (Coq_config.version,date) in
+  let (rev,ver) = get_version_date () in
+    Printf.sprintf 
+      "The Coq Proof Assistant, version %s (%s)\
+       \nArchitecture %s running %s operating system\
+       \nGtk version is %s\
+       \nThis is the %s version (%s is the best one for this architecture and OS)\
+       \n"
+      rev ver
+      Coq_config.arch Sys.os_type
+      (let x,y,z = GMain.Main.version in Printf.sprintf "%d.%d.%d" x y z)
     (if Mltop.get () = Mltop.Native then "native" else "bytecode") 
     (if Coq_config.best="opt" then "native" else "bytecode") 
 
 let is_in_coq_lib dir = 
   prerr_endline ("Is it a coq theory ? : "^dir);
-  try
-    let stat = Unix.stat dir in
-      List.exists 
-	(fun s -> 
-	   try
-	     let fdir = Filename.concat 
-	       Coq_config.coqlib 
-	       (Filename.concat "theories" s) 
-	     in
-	       prerr_endline (" Comparing to: "^fdir);
-	       let fstat = Unix.stat fdir in 
-		 (fstat.Unix.st_dev = stat.Unix.st_dev) &&
-		   (fstat.Unix.st_ino = stat.Unix.st_ino) && 
-		   (prerr_endline " YES";true)
-	   with _ -> prerr_endline " No(because of a local exn)";false
-	)
-	Coq_config.theories_dirs
-  with _ -> prerr_endline " No(because of a global exn)";false
-
-let is_in_loadpath dir = Library.is_in_load_paths (System.physical_path_of_string dir)
+  let is_same_file = same_file dir in
+  List.exists 
+    (fun s -> 
+      let fdir =
+        Filename.concat Coq_config.coqlib (Filename.concat "theories" s) in
+      prerr_endline (" Comparing to: "^fdir);
+      if is_same_file fdir then (prerr_endline " YES";true)
+      else (prerr_endline"NO";false))
+    Coq_config.theories_dirs
+
+let is_in_loadpath dir =
+  Library.is_in_load_paths (System.physical_path_of_string dir)
 
 let is_in_coq_path f = 
   try 
@@ -104,7 +103,9 @@ let is_in_coq_path f =
     false  
 
 let is_in_proof_mode () = 
-  try ignore (get_pftreestate ()); true with _ -> false
+  match Decl_mode.get_current_mode () with
+      Decl_mode.Mode_none -> false
+    | _ -> true
 
 let user_error_loc l s =
   raise (Stdpp.Exc_located (l, Util.UserError ("CoqIde", s)))
@@ -246,12 +247,13 @@ type hyp = env * evar_map *
            ((identifier * string) * constr option * constr) * 
            (string * string)
 type concl = env * evar_map * constr * string
+type meta = env * evar_map * string
 type goal = hyp list * concl
 
 let prepare_hyp sigma env ((i,c,d) as a) =
   env, sigma,
   ((i,string_of_id i),c,d), 
-  (msg (pr_var_decl env a), msg (pr_lconstr_env_at_top env d))
+  (msg (pr_var_decl env a), msg (pr_ltype_env env d))
 
 let prepare_hyps sigma env =
   assert (rel_context env = []);
@@ -265,7 +267,38 @@ let prepare_hyps sigma env =
 let prepare_goal sigma g =
   let env = evar_env g in
   (prepare_hyps sigma env,
-   (env, sigma, g.evar_concl, msg (pr_lconstr_env_at_top env g.evar_concl)))
+   (env, sigma, g.evar_concl, msg (pr_ltype_env_at_top env g.evar_concl)))
+
+let prepare_hyps_filter info sigma env =
+  assert (rel_context env = []);
+  let hyps =
+    fold_named_context
+      (fun env ((id,_,_) as d) acc ->
+	 if true || Idset.mem id info.pm_hyps then
+	   let hyp = prepare_hyp sigma env d in hyp :: acc
+	 else acc)
+      env ~init:[] 
+  in
+  List.rev hyps
+
+let prepare_meta sigma env (m,typ)  =
+  env, sigma, 
+  (msg (str " ?" ++ int m ++ str " : " ++ pr_ltype_env_at_top env typ))
+
+let prepare_metas info sigma env =
+  List.fold_right 
+    (fun cpl acc ->  
+      let meta = prepare_meta sigma env cpl in meta :: acc)
+    info.pm_subgoals [] 
+
+let get_current_pm_goal () =
+  let pfts = get_pftreestate ()  in
+  let gls = try nth_goal_of_pftreestate 1 pfts with _ -> raise Not_found in
+  let info = Decl_mode.get_info gls.it in
+  let env = pf_env gls in
+  let sigma= sig_sig gls in
+    (prepare_hyps_filter info sigma env,
+     prepare_metas info sigma env)
 
 let get_current_goals () = 
     let pfts = get_pftreestate () in
@@ -275,14 +308,13 @@ let get_current_goals () =
 
 let get_current_goals_nb () = 
   try List.length (get_current_goals ()) with _ -> 0
-
   
 let print_no_goal () =
     let pfts = get_pftreestate () in
     let gls = fst (Refiner.frontier (Tacmach.proof_of_pftreestate pfts)) in 
     assert (gls = []);
     let sigma = Tacmach.project (Tacmach.top_goal_of_pftreestate pfts) in
-    msg (Printer.pr_subgoals sigma gls)
+    msg (Printer.pr_subgoals (Decl_mode.get_end_command pfts) sigma gls)
 
 
 type word_class = Normal | Kwd | Reserved
@@ -335,7 +367,7 @@ let compute_reset_info = function
   | VernacDeclareModule (_,(_,id), _, _)
   | VernacDeclareModuleType ((_,id), _, _)
   | VernacAssumption (_, (_,((_,id)::_,_))::_)
-  | VernacInductive (_, ((_,id),_,_,_,_) :: _) ->
+  | VernacInductive (_, (((_,id),_,_,_),_) :: _) ->
       Reset (id, ref true)
   | VernacDefinition (_, (_,id), ProveBody _, _)
   | VernacStartTheoremProof (_, (_,id), _, _, _) ->
diff --git a/ide/coq.mli b/ide/coq.mli
index 666a5397..4b4c3267 100644
--- a/ide/coq.mli
+++ b/ide/coq.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: coq.mli 8877 2006-05-30 16:37:04Z notin $ i*)
+(*i $Id: coq.mli 9154 2006-09-20 17:18:18Z corbinea $ i*)
 
 open Names
 open Term
@@ -27,11 +27,14 @@ val is_state_preserving : Vernacexpr.vernac_expr -> bool
 
 type hyp = env * evar_map * 
            ((identifier*string) * constr option * constr) * (string * string)
+type meta = env * evar_map * string
 type concl = env * evar_map * constr * string
 type goal = hyp list * concl
 
 val get_current_goals : unit -> goal list
 
+val get_current_pm_goal : unit -> hyp list * meta list
+
 val get_current_goals_nb : unit -> int
 
 val print_no_goal : unit -> string
diff --git a/ide/coqide.ml b/ide/coqide.ml
index cfde925d..fb650cbf 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: coqide.ml 8932 2006-06-09 09:29:03Z notin $ *)
+(* $Id: coqide.ml 9307 2006-10-28 18:48:48Z herbelin $ *)
 
 open Preferences
 open Vernacexpr
@@ -175,8 +175,9 @@ object('self)
   method reset_initial : unit
   method send_to_coq :
     bool -> bool -> string ->
-    bool -> bool -> bool -> (Util.loc * Vernacexpr.vernac_expr) option
+    bool -> bool -> bool -> (bool*(Util.loc * Vernacexpr.vernac_expr)) option
   method set_message : string -> unit
+  method show_pm_goal : unit
   method show_goals : unit
   method show_goals_full : unit
   method undo_last_step : unit
@@ -327,10 +328,10 @@ let remove_current_view_page () =
     kill_input_view c;
     ((notebook ())#get_nth_page c)#misc#hide ()
 
+let is_word_char c =
+  (* TODO: avoid num and prime at the head of a word *)
+  Glib.Unichar.isalnum c || c = underscore || c = prime
 
-let is_word_char c = 
-  Glib.Unichar.isalnum c || c = underscore || c = prime || c = arobase
-  
 let starts_word it = 
   prerr_endline ("Starts word ? '"^(Glib.Utf8.from_unichar it#char)^"'");
   (not it#copy#nocopy#backward_char ||
@@ -340,14 +341,14 @@ let starts_word it =
 let ends_word it = 
   (not it#copy#nocopy#forward_char ||
      let c = it#forward_char#char in
-       not (Glib.Unichar.isalnum c || c = underscore || c = prime || c = arobase)
+       not (is_word_char c)
   )
 
 let inside_word it = 
   let c = it#char in
     not (starts_word it) &&
       not (ends_word it) &&
-      (Glib.Unichar.isalnum c || c = underscore || c = prime || c = arobase)
+      is_word_char c
 
 let is_on_word_limit it = inside_word it || ends_word it 
 
@@ -789,50 +790,88 @@ object(self)
 		  (String.make previous_line_spaces ' ')
 	end
 
+  method show_pm_goal = 
+      proof_buffer#insert 
+	(Printf.sprintf "    *** Declarative Mode ***\n");
+      try 
+	let (hyps,metas) = get_current_pm_goal () in
+	List.iter
+	  (fun ((_,_,_,(s,_)) as _hyp) -> 
+	     proof_buffer#insert (s^"\n"))
+	  hyps;
+	proof_buffer#insert 
+	  (String.make 38 '_' ^ "\n");
+	List.iter
+	  (fun (_,_,m) -> 
+	     proof_buffer#insert (m^"\n"))
+	  metas;
+	let my_mark = `NAME "end_of_conclusion" in
+	  proof_buffer#move_mark
+	    ~where:((proof_buffer#get_iter_at_mark `INSERT)) 
+	    my_mark;
+	  ignore (proof_view#scroll_to_mark my_mark) 
+    with Not_found ->  
+      match Decl_mode.get_end_command (Pfedit.get_pftreestate ()) with
+	  Some endc ->
+	    proof_buffer#insert 
+	      ("Subproof completed, now type "^endc^".") 
+	| None ->
+	    proof_buffer#insert "Proof completed."
 
   method show_goals = 
     try
       proof_view#buffer#set_text "";
-      let s = Coq.get_current_goals () in
-	match s with 
-	  | [] -> proof_buffer#insert (Coq.print_no_goal ())
-	  | (hyps,concl)::r -> 
-	      let goal_nb = List.length s in
-		proof_buffer#insert (Printf.sprintf "%d subgoal%s\n" 
-				       goal_nb
-				       (if goal_nb<=1 then "" else "s"));
-		List.iter
-		  (fun ((_,_,_,(s,_)) as _hyp) -> 
-		     proof_buffer#insert (s^"\n"))
-		  hyps;
-		proof_buffer#insert (String.make 38 '_' ^ "(1/"^
-				       (string_of_int goal_nb)^
-				       ")\n") 
-		;
-		let _,_,_,sconcl = concl in
-		  proof_buffer#insert sconcl;
-		  proof_buffer#insert "\n";
-		  let my_mark = `NAME "end_of_conclusion" in
-		    proof_buffer#move_mark
-		      ~where:((proof_buffer#get_iter_at_mark `INSERT)) my_mark;
-		    proof_buffer#insert "\n\n";
-		    let i = ref 1 in
-		      List.iter 
-			(function (_,(_,_,_,concl)) -> 
-			   incr i;
-			   proof_buffer#insert (String.make 38 '_' ^"("^
-						  (string_of_int !i)^
-						  "/"^
-						  (string_of_int goal_nb)^
-						  ")\n");
-			   proof_buffer#insert concl;
-			   proof_buffer#insert "\n\n";
-			)
-			r;
-		      ignore (proof_view#scroll_to_mark my_mark) 
-    with e -> prerr_endline ("Don't worry be happy despite: "^Printexc.to_string e)
-      
-
+      match Decl_mode.get_current_mode () with
+	  Decl_mode.Mode_none ->  proof_buffer#insert (Coq.print_no_goal ())
+	| Decl_mode.Mode_tactic ->   
+	    begin
+	      let s = Coq.get_current_goals () in
+		match s with 
+		  | [] -> proof_buffer#insert (Coq.print_no_goal ())
+		  | (hyps,concl)::r -> 
+		      let goal_nb = List.length s in
+			proof_buffer#insert 
+			  (Printf.sprintf "%d subgoal%s\n" 
+			     goal_nb
+			     (if goal_nb<=1 then "" else "s"));
+			List.iter
+			  (fun ((_,_,_,(s,_)) as _hyp) -> 
+			     proof_buffer#insert (s^"\n"))
+			  hyps;
+			proof_buffer#insert 
+			  (String.make 38 '_' ^ "(1/"^
+			     (string_of_int goal_nb)^
+			     ")\n") ;
+			let _,_,_,sconcl = concl in
+			  proof_buffer#insert sconcl;
+			  proof_buffer#insert "\n";
+			  let my_mark = `NAME "end_of_conclusion" in
+			    proof_buffer#move_mark
+			      ~where:((proof_buffer#get_iter_at_mark `INSERT)) 
+			      my_mark;
+			    proof_buffer#insert "\n\n";
+			    let i = ref 1 in
+			      List.iter 
+				(function (_,(_,_,_,concl)) -> 
+				   incr i;
+				   proof_buffer#insert 
+				     (String.make 38 '_' ^"("^
+					(string_of_int !i)^
+					"/"^
+					(string_of_int goal_nb)^
+					")\n");
+				   proof_buffer#insert concl;
+				   proof_buffer#insert "\n\n";
+				)
+				r;
+			      ignore (proof_view#scroll_to_mark my_mark) 
+	    end
+	| Decl_mode.Mode_proof -> 
+	    self#show_pm_goal
+    with e -> 
+      prerr_endline ("Don't worry be happy despite: "^Printexc.to_string e)
+	
+	      
   val mutable full_goal_done = true
 
   method show_goals_full = 
@@ -840,148 +879,160 @@ object(self)
       begin
 	try
 	  proof_view#buffer#set_text "";
-	  let s = Coq.get_current_goals () in
-	  let last_shown_area = proof_buffer#create_tag [`BACKGROUND "light green"]
-	  in
-	    match s with 
-	      | [] -> proof_buffer#insert (Coq.print_no_goal ())
-	      | (hyps,concl)::r -> 
-		  let goal_nb = List.length s in
-		    proof_buffer#insert (Printf.sprintf "%d subgoal%s\n" 
-					   goal_nb
-					   (if goal_nb<=1 then "" else "s"));
-		    let coq_menu commands = 
-		      let tag = proof_buffer#create_tag []
-		      in 
-			ignore
-			  (tag#connect#event ~callback:
-			     (fun ~origin ev it ->
-				begin match GdkEvent.get_type ev with 
-				  | `BUTTON_PRESS -> 
-				      let ev = (GdkEvent.Button.cast ev) in
-					if (GdkEvent.Button.button ev) = 3
-					then begin 
-					    let loc_menu = GMenu.menu () in
-					    let factory = new GMenu.factory loc_menu in
-					    let add_coq_command (cp,ip) = 
-					      ignore 
-						(factory#add_item cp 
-						   ~callback:
-						   (fun () -> ignore
-						      (self#insert_this_phrase_on_success 
-							 true
-							 true 
-							 false 
-							 ("progress "^ip^"\n") 
-							 (ip^"\n"))
-						   )
-						)
-					    in
-					      List.iter add_coq_command commands;
-					      loc_menu#popup 
-						~button:3
-						~time:(GdkEvent.Button.time ev);
-					  end
-				  | `MOTION_NOTIFY -> 
-				      proof_buffer#remove_tag
-					~start:proof_buffer#start_iter
-					~stop:proof_buffer#end_iter
-					last_shown_area;
-				      prerr_endline "Before find_tag_limits";
-				      
-				      let s,e = find_tag_limits tag 
+	  match Decl_mode.get_current_mode () with
+	      Decl_mode.Mode_none ->  
+		proof_buffer#insert (Coq.print_no_goal ())
+	    | Decl_mode.Mode_tactic ->   
+		begin
+		  match Coq.get_current_goals () with 
+		      [] -> Util.anomaly "show_goals_full"
+		  | ((hyps,concl)::r) as s ->
+		      let last_shown_area = 
+			proof_buffer#create_tag [`BACKGROUND "light green"]
+		      in
+		      let goal_nb = List.length s in
+			proof_buffer#insert (Printf.sprintf "%d subgoal%s\n" 
+					 goal_nb
+					 (if goal_nb<=1 then "" else "s"));
+		  let coq_menu commands = 
+		    let tag = proof_buffer#create_tag []
+		    in 
+		      ignore
+			(tag#connect#event ~callback:
+			   (fun ~origin ev it ->
+			      begin match GdkEvent.get_type ev with 
+				| `BUTTON_PRESS -> 
+				    let ev = (GdkEvent.Button.cast ev) in
+				      if (GdkEvent.Button.button ev) = 3
+				      then begin 
+					let loc_menu = GMenu.menu () in
+					let factory = 
+					  new GMenu.factory loc_menu in
+					let add_coq_command (cp,ip) = 
+					  ignore 
+					    (factory#add_item cp 
+					       ~callback:
+				     (fun () -> ignore
+					(self#insert_this_phrase_on_success 
+					   true
+					   true 
+					   false 
+					   ("progress "^ip^"\n") 
+					   (ip^"\n"))
+				     )
+				  )
+			      in
+			      List.iter add_coq_command commands;
+			      loc_menu#popup 
+				~button:3
+				~time:(GdkEvent.Button.time ev);
+			    end
+			| `MOTION_NOTIFY -> 
+			    proof_buffer#remove_tag
+			    ~start:proof_buffer#start_iter
+			    ~stop:proof_buffer#end_iter
+			    last_shown_area;
+			    prerr_endline "Before find_tag_limits";
+			    
+			    let s,e = find_tag_limits tag 
 					(new GText.iter it) 
-				      in
-					prerr_endline "After find_tag_limits";
-					proof_buffer#apply_tag 
-					  ~start:s 
-					  ~stop:e 
-					  last_shown_area;
-					
-					prerr_endline "Applied tag";
-					()
-				  | _ -> ()
-				end;false
-			     )
-			  );
-			tag
-		    in
-		      List.iter
-			(fun ((_,_,_,(s,_)) as hyp) -> 
-			   let tag = coq_menu (hyp_menu hyp) in
-			     proof_buffer#insert ~tags:[tag] (s^"\n"))
-			hyps;
-		      proof_buffer#insert 
-			(String.make 38 '_' ^"(1/"^
-			   (string_of_int goal_nb)^
-			   ")\n") 
-		      ;
-		      let tag = coq_menu (concl_menu concl) in
-		      let _,_,_,sconcl = concl in
-			proof_buffer#insert ~tags:[tag] sconcl;
-			proof_buffer#insert "\n";
-			let my_mark = `NAME "end_of_conclusion" in
-			  proof_buffer#move_mark
-			    ~where:((proof_buffer#get_iter_at_mark `INSERT)) my_mark;
-			  proof_buffer#insert "\n\n";
-			  let i = ref 1 in
-			    List.iter 
-			      (function (_,(_,_,_,concl)) -> 
-				 incr i;
-				 proof_buffer#insert 
-				   (String.make 38 '_' ^"("^
-				      (string_of_int !i)^
-				      "/"^
-				      (string_of_int goal_nb)^
-				      ")\n");
-				 proof_buffer#insert concl;
-				 proof_buffer#insert "\n\n";
-			      )
-			      r;
-			    ignore (proof_view#scroll_to_mark my_mark) ;
-			    full_goal_done <- true;
-	with e -> prerr_endline (Printexc.to_string e)
+			    in
+			    prerr_endline "After find_tag_limits";
+			    proof_buffer#apply_tag 
+			      ~start:s 
+			      ~stop:e 
+			      last_shown_area;
+			    
+			    prerr_endline "Applied tag";
+			    ()
+			| _ -> ()
+			end;false
+		     )
+		  );
+		tag
+	      in
+	      List.iter
+		(fun ((_,_,_,(s,_)) as hyp) -> 
+		   let tag = coq_menu (hyp_menu hyp) in
+		   proof_buffer#insert ~tags:[tag] (s^"\n"))
+		hyps;
+	      proof_buffer#insert 
+		(String.make 38 '_' ^"(1/"^
+		 (string_of_int goal_nb)^
+		 ")\n") 
+	      ;
+	      let tag = coq_menu (concl_menu concl) in
+	      let _,_,_,sconcl = concl in
+	      proof_buffer#insert ~tags:[tag] sconcl;
+	      proof_buffer#insert "\n";
+	      let my_mark = `NAME "end_of_conclusion" in
+	      proof_buffer#move_mark
+		~where:((proof_buffer#get_iter_at_mark `INSERT)) my_mark;
+	      proof_buffer#insert "\n\n";
+	      let i = ref 1 in
+	      List.iter 
+		(function (_,(_,_,_,concl)) -> 
+		   incr i;
+		   proof_buffer#insert 
+		     (String.make 38 '_' ^"("^
+		      (string_of_int !i)^
+		      "/"^
+		      (string_of_int goal_nb)^
+		      ")\n");
+		   proof_buffer#insert concl;
+		   proof_buffer#insert "\n\n";
+		)
+		r;
+		ignore (proof_view#scroll_to_mark my_mark) ;
+		full_goal_done <- true
+		end
+	    | Decl_mode.Mode_proof ->
+		self#show_pm_goal
+	  with e -> prerr_endline (Printexc.to_string e)
       end
-	
+      
   method send_to_coq verbosely replace phrase show_output show_error localize =
     let display_output msg =
       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 Util.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_by_name "error"
-   		     ~start:starti
-		     ~stop:stopi;
-		   input_buffer#place_cursor starti) in
-      try 
-	full_goal_done <- false;
-	prerr_endline "Send_to_coq starting now";
-	if replace then begin
-	    let r,info = Coq.interp_and_replace ("info " ^ phrase) in
-	    let msg = read_stdout () in
-              sync display_output msg;
-	      Some r	
-	  end else begin
-	      let r = Coq.interp verbosely phrase in
-	      let msg = read_stdout () in
-		sync display_output msg;
-		Some r
-	    end
-      with e ->
-	if show_error then sync display_error e;
-	None
+      assert (Glib.Utf8.validate s);
+      self#insert_message s;
+      message_view#misc#draw None;
+      if localize then 
+	(match Util.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_by_name "error"
+   		~start:starti
+		~stop:stopi;
+	      input_buffer#place_cursor starti) in
+    try 
+      full_goal_done <- false;
+      prerr_endline "Send_to_coq starting now";
+      Decl_mode.clear_daimon_flag ();
+      if replace then begin
+	let r,info = Coq.interp_and_replace ("info " ^ phrase) in
+	let complete = not (Decl_mode.get_daimon_flag ()) in 
+	let msg = read_stdout () in
+        sync display_output msg;
+	Some (complete,r)	
+      end else begin
+	let r = Coq.interp verbosely phrase in
+	let complete = not (Decl_mode.get_daimon_flag ()) in 
+	let msg = read_stdout () in
+        sync display_output msg;
+        Some (complete,r)
+      end
+    with e ->
+      if show_error then sync display_error e;
+      None
 
   method find_phrase_starting_at (start:GText.iter) = 
     prerr_endline "find_phrase_starting_at starting now";
@@ -1018,7 +1069,7 @@ object(self)
     in
       try
 	trash_bytes := "";
-	let phrase = Find_phrase.get (Lexing.from_function lexbuf_function) 
+	let _ = Find_phrase.get (Lexing.from_function lexbuf_function) 
 	in
 	  end_iter#nocopy#set_offset (start#offset + !Find_phrase.length);
 	  Some (start,end_iter)
@@ -1089,10 +1140,11 @@ object(self)
 	  input_view#set_editable true;
 	  !pop_info ();
 	end in
-    let mark_processed (start,stop) ast =
-      let b = input_buffer in
+      let mark_processed complete (start,stop) ast =
+        let b = input_buffer in
 	b#move_mark ~where:stop (`NAME "start_of_input");
-	b#apply_tag_by_name "processed" ~start ~stop;
+	b#apply_tag_by_name 
+	  (if complete then "processed" else "unjustified") ~start ~stop;
 	if (self#get_insert#compare) stop <= 0 then 
 	  begin
 	    b#place_cursor stop;
@@ -1100,67 +1152,69 @@ object(self)
 	  end;
 	let start_of_phrase_mark = `MARK (b#create_mark start) in
 	let end_of_phrase_mark = `MARK (b#create_mark stop) in
-	  push_phrase 
-	    start_of_phrase_mark 
-	    end_of_phrase_mark ast;
-	  if display_goals then self#show_goals;
-          remove_tag (start,stop) in
+	push_phrase 
+	  start_of_phrase_mark 
+	  end_of_phrase_mark ast;
+	if display_goals then self#show_goals;
+        remove_tag (start,stop) in
       begin
         match sync get_next_phrase () with
             None -> false
           | Some (loc,phrase) ->
-              (match self#send_to_coq verbosely false phrase true true true with
-		 | Some ast -> sync (mark_processed loc) ast; true
-		 | None -> sync remove_tag loc; false)
+            (match self#send_to_coq verbosely false phrase true true true with
+	      | Some (complete,ast) -> 
+		  sync (mark_processed complete) loc ast; true
+	      | None -> sync remove_tag loc; false)
       end
-	
+    
   method insert_this_phrase_on_success 
     show_output show_msg localize coqphrase insertphrase = 
-    let mark_processed ast =
+    let mark_processed complete ast =
       let stop = self#get_start_of_input in
-	if stop#starts_line then
-	  input_buffer#insert ~iter:stop insertphrase
-	else input_buffer#insert ~iter:stop ("\n"^insertphrase); 
-	let start = self#get_start_of_input in
-	  input_buffer#move_mark ~where:stop (`NAME "start_of_input");
-	  input_buffer#apply_tag_by_name "processed" ~start ~stop;
-	  if (self#get_insert#compare) stop <= 0 then 
-	    input_buffer#place_cursor stop;
-	  let start_of_phrase_mark = `MARK (input_buffer#create_mark start) in
-	  let end_of_phrase_mark = `MARK (input_buffer#create_mark stop) in
-	    push_phrase start_of_phrase_mark end_of_phrase_mark ast;
-	    self#show_goals;
-	    (*Auto insert save on success... 
-	      try (match Coq.get_current_goals () with 
-	      | [] ->  
-	      (match self#send_to_coq "Save.\n" true true true with
+      if stop#starts_line then
+	input_buffer#insert ~iter:stop insertphrase
+      else input_buffer#insert ~iter:stop ("\n"^insertphrase); 
+      let start = self#get_start_of_input in
+      input_buffer#move_mark ~where:stop (`NAME "start_of_input");
+      input_buffer#apply_tag_by_name 
+	(if complete then "processed" else "unjustified") ~start ~stop;
+      if (self#get_insert#compare) stop <= 0 then 
+	input_buffer#place_cursor stop;
+      let start_of_phrase_mark = `MARK (input_buffer#create_mark start) in
+      let end_of_phrase_mark = `MARK (input_buffer#create_mark stop) in
+      push_phrase start_of_phrase_mark end_of_phrase_mark ast;
+      self#show_goals;
+      (*Auto insert save on success... 
+      try (match Coq.get_current_goals () with 
+	| [] ->  
+	    (match self#send_to_coq "Save.\n" true true true with
 	      | Some ast -> 
-	      begin
-              let stop = self#get_start_of_input in
-	      if stop#starts_line then
-	      input_buffer#insert ~iter:stop "Save.\n"
-	      else input_buffer#insert ~iter:stop "\nSave.\n"; 
-	      let start = self#get_start_of_input in
-	      input_buffer#move_mark ~where:stop (`NAME"start_of_input");
-	      input_buffer#apply_tag_by_name "processed" ~start ~stop;
-	      if (self#get_insert#compare) stop <= 0 then 
-	      input_buffer#place_cursor stop;
-	      let start_of_phrase_mark =
-              `MARK (input_buffer#create_mark start) in
-	      let end_of_phrase_mark =
-              `MARK (input_buffer#create_mark stop) in
-	      push_phrase start_of_phrase_mark end_of_phrase_mark ast
-	      end
+	          begin
+                    let stop = self#get_start_of_input in
+	            if stop#starts_line then
+	              input_buffer#insert ~iter:stop "Save.\n"
+	            else input_buffer#insert ~iter:stop "\nSave.\n"; 
+	            let start = self#get_start_of_input in
+	            input_buffer#move_mark ~where:stop (`NAME"start_of_input");
+	            input_buffer#apply_tag_by_name "processed" ~start ~stop;
+	            if (self#get_insert#compare) stop <= 0 then 
+	              input_buffer#place_cursor stop;
+	            let start_of_phrase_mark =
+                      `MARK (input_buffer#create_mark start) in
+	            let end_of_phrase_mark =
+                      `MARK (input_buffer#create_mark stop) in
+	            push_phrase start_of_phrase_mark end_of_phrase_mark ast
+	          end
 	      | None -> ())
-	      | _ -> ())
-	      with _ -> ()*) in
-      match self#send_to_coq false false coqphrase show_output show_msg localize with
-	| Some ast -> sync mark_processed ast; true
-	| None ->
-            sync
-              (fun _ -> self#insert_message ("Unsuccessfully tried: "^coqphrase))
-              ();
-	    false
+	| _ -> ())
+      with _ -> ()*) in
+    match self#send_to_coq false false coqphrase show_output show_msg localize with
+      | Some (complete,ast) -> sync (mark_processed complete) ast; true
+      | None ->
+          sync
+            (fun _ -> self#insert_message ("Unsuccessfully tried: "^coqphrase))
+            ();
+	  false
 
   method process_until_iter_or_error stop =
     let stop' = `OFFSET stop#offset in
@@ -1170,20 +1224,29 @@ object(self)
 	      input_buffer#apply_tag_by_name ~start ~stop "to_process";
 	      input_view#set_editable false) ();
       !push_info "Coq is computing";
-      (try 
-	   while ((stop#compare self#get_start_of_input>=0) 
-		  && (self#process_next_phrase false false false))
-	   do Util.check_for_interrupt () done
-       with Sys.Break -> 
-	 prerr_endline "Interrupted during process_until_iter_or_error");
-      sync (fun _ ->
-	      self#show_goals;
-	      (* Start and stop might be invalid if an eol was added at eof *)
-	      let start = input_buffer#get_iter start' in
-	      let stop =  input_buffer#get_iter stop' in
-		input_buffer#remove_tag_by_name ~start ~stop "to_process" ;
-		input_view#set_editable true) ();
-      !pop_info()
+      let get_current () =
+	if !current.stop_before then
+          match self#find_phrase_starting_at self#get_start_of_input with
+            | None -> self#get_start_of_input
+            | Some (_, stop2) -> stop2
+	else begin
+            self#get_start_of_input
+	  end
+      in   
+	(try 
+	    while ((stop#compare (get_current())>=0) 
+		    && (self#process_next_phrase false false false))
+	    do Util.check_for_interrupt () done
+	  with Sys.Break -> 
+	    prerr_endline "Interrupted during process_until_iter_or_error");
+	sync (fun _ ->
+	  self#show_goals;
+	  (* Start and stop might be invalid if an eol was added at eof *)
+	  let start = input_buffer#get_iter start' in
+	  let stop =  input_buffer#get_iter stop' in
+	    input_buffer#remove_tag_by_name ~start ~stop "to_process" ;
+	    input_view#set_editable true) ();
+	!pop_info()
 
   method process_until_end_or_error = 
     self#process_until_iter_or_error input_buffer#end_iter
@@ -1196,6 +1259,7 @@ object(self)
 		 let stop = input_buffer#get_iter_at_mark inf.stop in
 		   input_buffer#move_mark ~where:start (`NAME "start_of_input");
 		   input_buffer#remove_tag_by_name "processed" ~start ~stop;
+		   input_buffer#remove_tag_by_name "unjustified" ~start ~stop;
 		   input_buffer#delete_mark inf.start;
 		   input_buffer#delete_mark inf.stop;
               ) 
@@ -1260,6 +1324,10 @@ object(self)
 			~start 
 			~stop:self#get_start_of_input
 			"processed";
+		      input_buffer#remove_tag_by_name 
+			~start 
+			~stop:self#get_start_of_input
+			"unjustified";
 		      prerr_endline "Moving (long) start_of_input...";
 		      input_buffer#move_mark ~where:start (`NAME "start_of_input");
 		      self#show_goals;
@@ -1269,9 +1337,9 @@ object(self)
 	  with _ -> 
 	    !push_info "WARNING: undo failed badly -> Coq might be in an inconsistent state.
 Please restart and report NOW.";
-	end
-      else prerr_endline "backtrack_to : discarded (...)"
-	
+      end
+    else prerr_endline "backtrack_to : discarded (...)"
+      
   method backtrack_to i = 
     if Mutex.try_lock coq_may_stop then 
       (!push_info "Undoing...";self#backtrack_to_no_lock i ; Mutex.unlock coq_may_stop;
@@ -1296,6 +1364,10 @@ Please restart and report NOW.";
 		~start
 		~stop:(input_buffer#get_iter_at_mark last_command.stop) 
 		"processed";
+	      input_buffer#remove_tag_by_name 
+	        ~start
+	        ~stop:(input_buffer#get_iter_at_mark last_command.stop) 
+	      "unjustified";
 	      prerr_endline "Moving start_of_input";
 	      input_buffer#move_mark
 		~where:start
@@ -1356,6 +1428,7 @@ Please restart and report NOW.";
 		 let c = Blaster_window.present_blaster_window () in
 		   if Mutex.try_lock c#lock then begin
 		       c#clear ();
+                      Decl_mode.check_not_proof_mode "No blaster in Proof mode";
 		       let current_gls = try get_current_goals () with _ -> [] in
 			 
 		       let set_goal i (s,t) = 
@@ -1555,10 +1628,16 @@ Please restart and report NOW.";
 	      ~callback:(fun tag ~start ~stop ->
 			   if (start#compare self#get_start_of_input)>=0
 			   then 
-			     input_buffer#remove_tag_by_name 
-			       ~start
-			       ~stop
-			       "processed"
+			     begin
+			       input_buffer#remove_tag_by_name 
+				 ~start
+				 ~stop
+				 "processed";
+			       input_buffer#remove_tag_by_name 
+				 ~start
+				 ~stop
+				 "unjustified"
+			     end
 			)
 	   );
     ignore (input_buffer#connect#after#insert_text
@@ -1636,10 +1715,10 @@ end
 
 let create_input_tab filename =
   let b = GText.buffer () in 
-  let tablabel = GMisc.label () in 
+  let _ = GMisc.label () in 
   let v_box = GPack.hbox ~homogeneous:false () in
-  let image = GMisc.image ~packing:v_box#pack () in
-  let label = GMisc.label ~text:filename ~packing:v_box#pack () in
+  let _ = GMisc.image ~packing:v_box#pack () in
+  let _ = GMisc.label ~text:filename ~packing:v_box#pack () in
   let fr1 = GBin.frame ~shadow_type:`ETCHED_OUT
     ~packing:((notebook ())#append_page
 		~tab_label:v_box#coerce) () 
@@ -1694,6 +1773,10 @@ let create_input_tab filename =
       ignore (tv1#buffer#create_tag 
 		~name:"processed" 
 		[`BACKGROUND "light green" ;`EDITABLE false]);
+      ignore (tv1#buffer#create_tag (* Proof mode *)
+	        ~name:"unjustified" 
+               [`UNDERLINE `SINGLE ; `FOREGROUND "red";
+	         `BACKGROUND "gold" ;`EDITABLE false]);
       ignore (tv1#buffer#create_tag 
 		~name:"found" 
 		[`BACKGROUND "blue"; `FOREGROUND "white"]);
@@ -1933,7 +2016,8 @@ let main files =
 		ignore (revert_m#connect#activate revert_f);
 		
 		(* File/Close Menu *)
-		let close_m = file_factory#add_item "_Close Buffer" in
+		let close_m =
+                  file_factory#add_item "_Close Buffer" ~key:GdkKeysyms._W in
 		let close_f () = 
 		  let v = out_some !active_view in
 		  let act = get_current_view_page () in
@@ -1958,7 +2042,9 @@ let main files =
 			    let s,_ = run_command av#insert_message cmd in
 			      !flash_info (cmd ^ if s = Unix.WEXITED 0 then " succeeded" else " failed")
 		  in
-		  let print_m = file_factory#add_item "_Print" ~callback:print_f in
+		  let _ = file_factory#add_item "_Print"
+	            ~key:GdkKeysyms._P
+                    ~callback:print_f in
 
 		  (* File/Export to Menu *)
 		  let export_f kind () =
@@ -1989,16 +2075,16 @@ let main files =
 		  let file_export_m =  file_factory#add_submenu "E_xport to" in
 
 		  let file_export_factory = new GMenu.factory ~accel_path:"<CoqIde MenuBar>/Export/" file_export_m ~accel_group in
-		  let export_html_m = 
+		  let _ = 
 		    file_export_factory#add_item "_Html" ~callback:(export_f "html") 
 		  in
-		  let export_latex_m = 
+		  let _ = 
 		    file_export_factory#add_item "_LaTeX" ~callback:(export_f "latex")
 		  in
-		  let export_dvi_m = 
+		  let _ = 
 		    file_export_factory#add_item "_Dvi" ~callback:(export_f "dvi") 
 		  in
-		  let export_ps_m = 
+		  let _ = 
 		    file_export_factory#add_item "_Ps" ~callback:(export_f "ps") 
 		  in
 
@@ -2031,7 +2117,7 @@ let main files =
 			  | _ -> ()
 		      else exit 0
 		    in
-		    let quit_m = file_factory#add_item "_Quit" ~key:GdkKeysyms._Q 
+		    let _ = file_factory#add_item "_Quit" ~key:GdkKeysyms._Q 
 		      ~callback:quit_f
 		    in
 		      ignore (w#event#connect#delete (fun _ -> quit_f (); true));
@@ -2096,7 +2182,7 @@ let main files =
 			  ~col_spacings:10 ~row_spacings:10 ~border_width:10
 			  ~homogeneous:false ~packing:find_w#add () in
 			  
-			let find_lbl = 
+			let _ = 
 			  GMisc.label ~text:"Find:"
 			    ~xalign:1.0
 			    ~packing:(find_box#attach ~left:0 ~top:0 ~fill:`X) () 
@@ -2106,7 +2192,7 @@ let main files =
 			  ~packing: (find_box#attach ~left:1 ~top:0 ~expand:`X)
 			  ()
 			in
-			let replace_lbl = 
+			let _ = 
 			  GMisc.label ~text:"Replace with:"
 			    ~xalign:1.0
 			    ~packing:(find_box#attach ~left:0 ~top:1 ~fill:`X) () 
@@ -2116,7 +2202,7 @@ let main files =
 			  ~packing: (find_box#attach ~left:1 ~top:1 ~expand:`X)
 			  ()
 			in
-			let case_sensitive_check = 
+			let _ = 
 			  GButton.check_button
 			    ~label:"case sensitive"
 			    ~active:true
@@ -2268,11 +2354,11 @@ let main files =
 			    find_w#present ();
 			    find_entry#misc#grab_focus ()
 			  in
-			  let find_i = edit_f#add_item "_Find in buffer"
+			  let _ = edit_f#add_item "_Find in buffer"
 			    ~key:GdkKeysyms._F
 			    ~callback:(find_f ~backward:false)
 			  in
-			  let find_back_i = edit_f#add_item "Find _backwards"
+			  let _ = edit_f#add_item "Find _backwards"
 			    ~key:GdkKeysyms._B
 			    ~callback:(find_f ~backward:true)
 			  in
@@ -2365,7 +2451,7 @@ let main files =
 			      in reset_auto_save_timer (); (* to enable statup preferences timer *)
 
 
-				let edit_prefs_m =
+				let _ =
 				  edit_f#add_item "_Preferences"
 				    ~callback:(fun () -> configure ();reset_revert_timer ())
 				in
@@ -2417,10 +2503,14 @@ let main files =
 				  add_to_menu_toolbar 
 				    "_Save" 
 				    ~tooltip:"Save current buffer" 
-				    (* ~key:GdkKeysyms._Down *)
 				    ~callback:save_f
 				    `SAVE;
 				  add_to_menu_toolbar 
+				    "_Close" 
+				    ~tooltip:"Close current buffer" 
+				    ~callback:close_f
+				    `CLOSE;
+				  add_to_menu_toolbar 
 				    "_Forward" 
 				    ~tooltip:"Forward one command" 
 				    ~key:GdkKeysyms._Down 
@@ -2779,7 +2869,7 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S);
 							  av#insert_message res
 							end
 					  in
-					  let compile_m = 
+					  let _ = 
 					    externals_factory#add_item "_Compile Buffer" ~callback:compile_f 
 					  in
 
@@ -2796,7 +2886,7 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S);
 						last_make_index := 0;
 						!flash_info (!current.cmd_make ^ if s = Unix.WEXITED 0 then " succeeded" else " failed")
 					  in
-					  let make_m = externals_factory#add_item "_Make" 
+					  let _ = externals_factory#add_item "_Make" 
 					    ~key:GdkKeysyms._F6
 					    ~callback:make_f 
 					  in
@@ -2837,7 +2927,7 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S);
 					      let av = out_some v.analyzed_view in
 						av#set_message "No more errors.\n"
 					  in
-					  let next_error_m = 
+					  let _ = 
 					    externals_factory#add_item "_Next error" 
 					      ~key:GdkKeysyms._F7
 					      ~callback:next_error in
@@ -2857,7 +2947,7 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S);
 					  let configuration_menu = factory#add_submenu "_Windows" in
 					  let configuration_factory = new GMenu.factory configuration_menu ~accel_path:"<CoqIde MenuBar>/Windows" ~accel_group
 					  in
-					  let queries_show_m = 
+					  let _ = 
 					    configuration_factory#add_item 
 					      "Show _Query Window"
 					      (*
@@ -2865,14 +2955,14 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S);
 					      *)
 					      ~callback:(Command_windows.command_window ())#window#present
 					  in  
-					  let toolbar_show_m = 
+					  let _ = 
 					    configuration_factory#add_item 
 					      "Show/Hide _Toolbar"	       
 					      ~callback:(fun () ->  
 							   !current.show_toolbar <- not !current.show_toolbar; 
 							   !show_toolbar !current.show_toolbar) 
 					  in
-					  let detach_menu = configuration_factory#add_item 
+					  let _ = configuration_factory#add_item 
 					    "Detach _Script Window"
 					    ~callback:
 					    (do_if_not_computing "detach script window" (sync
@@ -2890,7 +2980,7 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S);
 												  end	      
 											   )))
 					  in
-					  let detach_current_view = 
+					  let _ = 
 					    configuration_factory#add_item 
 					      "Detach _View"
 					      ~callback:
@@ -3177,7 +3267,7 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S);
 						      let tv2 = GText.view ~packing:(sw2#add) () in
 							tv2#misc#set_name "GoalWindow";
 							let _ = tv2#set_editable false in
-							let tb2 = tv2#buffer in
+							let _ = tv2#buffer in
 							let tv3 = GText.view ~packing:(sw3#add) () in
 							  tv2#misc#set_name "MessageWindow";
 							  let _ = tv2#set_wrap_mode `CHAR in
diff --git a/ide/find_phrase.mll b/ide/find_phrase.mll
index 1621e313..23019185 100644
--- a/ide/find_phrase.mll
+++ b/ide/find_phrase.mll
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: find_phrase.mll 6218 2004-10-15 14:27:04Z coq $ *)
+(* $Id: find_phrase.mll 9240 2006-10-13 17:51:11Z notin $ *)
 
 {
   exception Lex_error of string
@@ -28,7 +28,11 @@ rule next_phrase = parse
 		 next_phrase lexbuf
 	       }
   | phrase_sep[' ''\n''\t''\r'] {
-      length := !length + 2; 
+	begin 
+	  if !Preferences.current.Preferences.lax_syntax 
+	  then length := !length + 1
+	  else length := !length + 2
+	end;
       Buffer.add_string buff (Lexing.lexeme lexbuf);
       Buffer.contents buff}
 
diff --git a/ide/ideutils.ml b/ide/ideutils.ml
index 65aef17f..df4594a7 100644
--- a/ide/ideutils.ml
+++ b/ide/ideutils.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: ideutils.ml 8912 2006-06-07 11:20:58Z notin $ *)
+(* $Id: ideutils.ml 9263 2006-10-23 12:08:08Z barras $ *)
 
 
 open Preferences
@@ -267,7 +267,7 @@ let run_command f c =
 
 let browse f url =
   let l,r = !current.cmd_browse in
-  let (s,res) = run_command f (l ^ url ^ r) in
+  let (_s,_res) = run_command f (l ^ url ^ r) in
   ()
 
 let url_for_keyword =
@@ -306,18 +306,27 @@ let tab = Glib.Utf8.to_unichar "\t" (ref 0)
 
 
 (*
-  checks if two file names refer to the same (existing) file
-*)
+  checks if two file names refer to the same (existing) file by
+  comparing their device and inode. 
+  It seems that under Windows, inode is always 0, so we cannot
+  accurately check if 
 
-let same_file f1 f2 =
+*)
+(* Optimised for partial application (in case many candidates must be
+   compared to f1). *)
+let same_file f1 =
   try
-    let s1 = Unix.stat f1
-    and s2 = Unix.stat f2 
-    in
-      (s1.Unix.st_dev = s2.Unix.st_dev) &&
-	(s1.Unix.st_ino = s2.Unix.st_ino) 
+    let s1 = Unix.stat f1 in
+    (fun f2 ->
+      try
+        let s2 = Unix.stat f2 in
+        s1.Unix.st_dev = s2.Unix.st_dev &&
+          if Sys.os_type = "Win32" then f1 = f2 
+          else s1.Unix.st_ino = s2.Unix.st_ino
+      with
+          Unix.Unix_error _ -> false)
   with
-      Unix.Unix_error _ -> false
+      Unix.Unix_error _ -> (fun _ -> false)
 
 let absolute_filename f =
   if Filename.is_relative f then 
diff --git a/ide/preferences.ml b/ide/preferences.ml
index 4cf9627c..c01fa602 100644
--- a/ide/preferences.ml
+++ b/ide/preferences.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: preferences.ml 8920 2006-06-08 09:12:48Z notin $ *)
+(* $Id: preferences.ml 9350 2006-11-07 15:04:42Z notin $ *)
 
 open Configwin
 open Printf
@@ -93,7 +93,9 @@ type pref =
       mutable use_utf8_notation : bool;
 *)
       mutable auto_complete : bool;
-    }
+      mutable stop_before : bool;
+      mutable lax_syntax : bool;
+}
 
 let (current:pref ref) = 
   ref {
@@ -118,9 +120,9 @@ let (current:pref ref) =
 			 "auto with *"; "intuition" ];
     
     modifier_for_navigation = [`CONTROL; `MOD1];
-    modifier_for_templates = [`MOD4];
+    modifier_for_templates = [`CONTROL; `SHIFT];
     modifier_for_tactics = [`CONTROL; `MOD1];
-    modifiers_valid = [`SHIFT; `CONTROL; `MOD1; `MOD4];
+    modifiers_valid = [`SHIFT; `CONTROL; `MOD1];
 
     
     cmd_browse = Options.browser_cmd_fmt;
@@ -143,7 +145,9 @@ let (current:pref ref) =
 (*
     use_utf8_notation = false;
 *)
-    auto_complete = false
+    auto_complete = false;
+    stop_before = true;
+    lax_syntax = true
   }
 
 
@@ -205,9 +209,11 @@ let save_pref () =
     add "query_window_height" [string_of_int p.query_window_height] ++
     add "query_window_width" [string_of_int p.query_window_width] ++
     add "auto_complete" [string_of_bool p.auto_complete] ++
+    add "stop_before" [string_of_bool p.stop_before] ++
+    add "lax_syntax" [string_of_bool p.lax_syntax] ++
     Config_lexer.print_file pref_file
   with _ -> prerr_endline "Could not save preferences."
-  
+ 
 
 let load_pref () =
   (try GtkData.AccelMap.load accel_file with _ -> ());
@@ -257,6 +263,8 @@ let load_pref () =
     set_int "query_window_width" (fun v -> np.query_window_width <- v);
     set_int "query_window_height" (fun v -> np.query_window_height <- v);
     set_bool "auto_complete" (fun v -> np.auto_complete <- v);
+    set_bool "stop_before" (fun v -> np.stop_before <- v);
+    set_bool "lax_syntax" (fun v -> np.lax_syntax <- v);
     current := np;
 (*
     Format.printf "in laod_pref: current.text_font = %s@." (Pango.Font.to_string !current.text_font);
@@ -385,6 +393,18 @@ let configure () =
       (string_of_int !current.auto_save_delay)
   in  
 
+  let stop_before =
+    bool
+      ~f:(fun s -> !current.stop_before <- s)
+      "Stop interpreting before the current point" !current.stop_before
+  in
+    
+  let lax_syntax =
+    bool
+      ~f:(fun s -> !current.lax_syntax <- s)
+      "Relax read-only constraint at end of command" !current.lax_syntax
+  in
+
   let encodings = 
     combo 
       "File charset encoding "
@@ -476,7 +496,7 @@ let configure () =
       "Contextual menus on goal" !current.contextual_menus_on_goal
   in 
 
-  let misc = [contextual_menus_on_goal;auto_complete] in
+  let misc = [contextual_menus_on_goal;auto_complete;stop_before;lax_syntax] in
    
 (* ATTENTION !!!!! L'onglet Fonts doit etre en premier pour eviter un bug !!!!
    (shame on Benjamin) *)
diff --git a/ide/preferences.mli b/ide/preferences.mli
index 25535aa4..c3e26f50 100644
--- a/ide/preferences.mli
+++ b/ide/preferences.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: preferences.mli 6621 2005-01-21 17:24:37Z herbelin $ i*)
+(*i $Id: preferences.mli 9240 2006-10-13 17:51:11Z notin $ i*)
 
 type pref =
     {
@@ -52,6 +52,8 @@ type pref =
       mutable use_utf8_notation : bool;
 *)
       mutable auto_complete : bool;
+      mutable stop_before : bool;
+      mutable lax_syntax : bool;
     }
 
 val save_pref : unit -> unit
diff --git a/ide/utils/editable_cells.ml b/ide/utils/editable_cells.ml
index e6d2f4d4..5441f4ab 100644
--- a/ide/utils/editable_cells.ml
+++ b/ide/utils/editable_cells.ml
@@ -85,7 +85,7 @@ let create l =
 			   | [] -> ()
 			   | path::_ ->
 			       let iter = store#get_iter path in
-			       GtkTree.TreePath.prev path;
+			       ignore (GtkTree.TreePath.prev path);
 			       let upiter = store#get_iter path in
 			       ignore (store#swap iter upiter);
 		      ));