Declarative Proof Language: main commit

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9154 85f007b7-540e-0410-9357-904b9bb8a0f7

4 files changed, 352 insertions, 241 deletions

diff --git a/ide/coq.ml b/ide/coq.ml
index f19cd91c9b..3d489dcb54 100644
--- a/ide/coq.ml
+++ b/ide/coq.ml
@@ -19,6 +19,7 @@ open Printer
 open Environ
 open Evarutil
 open Evd
+open Decl_mode
 open Hipattern
 open Tacmach
 open Reductionops
@@ -110,7 +111,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)))
@@ -252,6 +255,7 @@ 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) =
@@ -273,6 +277,37 @@ let prepare_goal sigma g =
   (prepare_hyps sigma env,
    (env, sigma, g.evar_concl, msg (pr_lconstr_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_lconstr_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
     let gls = fst (Refiner.frontier (Tacmach.proof_of_pftreestate pfts)) in 
@@ -281,14 +316,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
diff --git a/ide/coq.mli b/ide/coq.mli
index b6c0ed89cd..7b43a0c958 100644
--- a/ide/coq.mli
+++ b/ide/coq.mli
@@ -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 2d8291c146..b63cddd579 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -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
@@ -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";
@@ -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
@@ -1196,6 +1250,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 +1315,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 +1328,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 +1355,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 +1419,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 +1619,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
@@ -1694,6 +1764,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"]);
diff --git a/ide/utils/editable_cells.ml b/ide/utils/editable_cells.ml
index e6d2f4d48c..5441f4abe0 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);
 		      ));