coqide: blaster interruptible

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

4 files changed, 180 insertions, 104 deletions

diff --git a/ide/blaster_window.ml b/ide/blaster_window.ml
index 63b6c0675..83d900cc6 100644
--- a/ide/blaster_window.ml
+++ b/ide/blaster_window.ml
@@ -12,6 +12,9 @@ open Gobject.Data
 open Ideutils
 
 exception Stop
+exception Done
+
+module MyMap = Map.Make (struct type t = string let compare = compare end)
 
 class blaster_window (n:int) = 
   let window = GWindow.window 
@@ -49,13 +52,13 @@ class blaster_window (n:int) =
 	      ~renderer:(GTree.cell_renderer_text(), ["text",argument]) in
   let _ = view#append_column col in
   let col = GTree.view_column ~title:"Tactics" ()
-      ~renderer:(GTree.cell_renderer_text(), ["text",tactic]) in
+	      ~renderer:(GTree.cell_renderer_text(), ["text",tactic]) in
   let _ = view#append_column col in
   let col = GTree.view_column ~title:"Status" ()
-      ~renderer:(GTree.cell_renderer_toggle (), ["active",status]) in
+	      ~renderer:(GTree.cell_renderer_toggle (), ["active",status]) in
   let _ = view#append_column col in
   let col = GTree.view_column ~title:"Delta Goal" ()
-      ~renderer:(GTree.cell_renderer_text (), ["text",nb_goals]) in
+	      ~renderer:(GTree.cell_renderer_text (), ["text",nb_goals]) in
   let _ = view#append_column col in 
 
   let _ = GMisc.separator `HORIZONTAL ~packing:box1#pack () in
@@ -65,13 +68,14 @@ class blaster_window (n:int) =
   let button_stop = GButton.button ~label: "Stop" ~packing: box2#add () in
   let _ = button_stop#connect#clicked ~callback: window#misc#hide in
 
-  
 object(self)
   val window = window
   val roots = Hashtbl.create 17
-  val tbl = Hashtbl.create 17
+  val mutable tbl = MyMap.empty 
   val blaster_lock = Mutex.create () 
   method lock = blaster_lock 
+  val blaster_killed = Condition.create () 
+  method blaster_killed = blaster_killed
   method window = window
   method set
     root
@@ -79,45 +83,53 @@ object(self)
     (compute:unit -> Coq.tried_tactic) 
     (on_click:unit -> unit) 
     = 
-    let root = 
+    let root_iter = 
       try Hashtbl.find roots root 
       with Not_found -> 
 	let nr = new_arg root in
 	Hashtbl.add roots root nr;
 	nr
     in
-    let nt = new_tac root name in
-    Hashtbl.add tbl name (nt,compute,on_click)
+    let nt = new_tac root_iter name in
+    let old_val = try MyMap.find root tbl with Not_found -> MyMap.empty in
+    tbl <- MyMap.add root (MyMap.add name (nt,compute,on_click) old_val) tbl
 
   method clear () = 
     model#clear ();      
-    Hashtbl.clear tbl;
+    tbl <- MyMap.empty;
     Hashtbl.clear roots;
-
-      
+    
   method blaster () = 
-    if Mutex.try_lock blaster_lock then begin
-      view#expand_all ();
-      try Hashtbl.iter 
-	(fun k (nt,compute,on_click) ->
-	   match compute () with 
-	   | Coq.Interrupted -> 
-	       prerr_endline "Interrupted";
-	       raise Stop
-	   | Coq.Failed -> 
-	       prerr_endline "Failed";
-	       model#set ~row:nt ~column:status false;
-	       model#set ~row:nt ~column:nb_goals "N/A"
-	       
-	   | Coq.Success n -> 
-	       prerr_endline "Success";
-	       model#set ~row:nt ~column:status true;
-	       model#set ~row:nt ~column:nb_goals (string_of_int n)
-	)
-	tbl;
-      Mutex.unlock blaster_lock
-      with Stop -> Mutex.unlock blaster_lock
-    end else prerr_endline "blaster is till computing"
+    view#expand_all ();
+    try MyMap.iter 
+      (fun root_name l ->
+	 try 
+	   MyMap.iter 
+	     (fun name (nt,compute,on_click) ->  
+		match compute () with 
+		| Coq.Interrupted -> 
+		    prerr_endline "Interrupted";
+		    raise Stop
+		| Coq.Failed -> 
+		    prerr_endline "Failed";
+		    ignore (model#remove nt)
+		      (*	       model#set ~row:nt ~column:status false;
+				       model#set ~row:nt ~column:nb_goals "N/A"
+		      *)
+		| Coq.Success n -> 
+		    prerr_endline "Success";
+		    model#set ~row:nt ~column:status true;
+		    model#set ~row:nt ~column:nb_goals (string_of_int n);
+		    if n= -1 then raise Done 
+	     )
+	     l
+	 with Done -> ())
+      tbl;
+      Condition.signal blaster_killed;
+      prerr_endline "End of blaster";
+    with Stop ->
+      Condition.signal blaster_killed;
+      prerr_endline "End of blaster (stopped !)";
 
   initializer 
     ignore (window#event#connect#delete (fun _ -> window#misc#hide(); true));
@@ -125,26 +137,33 @@ object(self)
 	      begin fun () ->
 		prerr_endline "selection changed";
 		List.iter 
-		  (fun path -> prerr_endline (GtkTree.TreePath.to_string path);
+		  (fun path ->let pt = GtkTree.TreePath.to_string path in
 		     let it = model#get_iter path in
 		     prerr_endline (string_of_bool (model#iter_is_valid it));
-		     let name = model#get ~row:it ~column:tactic in
+		     let name = model#get 
+				  ~row:(if String.length pt >1 then begin
+					  ignore (GtkTree.TreePath.up path);
+					  model#get_iter path
+					end else it
+				       ) 
+				  ~column:argument in
+		     let tactic = model#get ~row:it ~column:tactic in
 		     prerr_endline ("Got name: "^name);
 		     let success = model#get ~row:it ~column:status in
 		     if success then try 
 		       prerr_endline "Got success";
-		       let _,_,f = Hashtbl.find tbl name in
+		       let _,_,f = MyMap.find tactic (MyMap.find name tbl) in
 		       f ();
-		       window#misc#hide ()
+		       (* window#misc#hide () *)
 		     with _ -> ()
 		  )
 		  view#selection#get_selected_rows
 	      end);
 
 (* needs lablgtk2 update    ignore (view#connect#after#row_activated
-	      (fun path vcol ->
-		 prerr_endline "Activated";
-);
+   (fun path vcol ->
+   prerr_endline "Activated";
+   );
 *)
 end
 
@@ -152,8 +171,13 @@ let blaster_window = ref None
 
 let main n = blaster_window := Some (new blaster_window n)
 
+let present_blaster_window () = match !blaster_window with 
+  | None -> failwith "No blaster window."
+  | Some c -> c#window#misc#show (* present*) (); c
+
+
 let blaster_window () = match !blaster_window with 
   | None -> failwith "No blaster window."
-  | Some c -> c#window#present (); c
+  | Some c -> c
 
 
diff --git a/ide/coq.ml b/ide/coq.ml
index 2df19fd77..e96017035 100644
--- a/ide/coq.ml
+++ b/ide/coq.ml
@@ -76,6 +76,7 @@ let is_in_proof_mode () =
 
 let interp s = 
   prerr_endline "Starting interp...";
+  prerr_endline s;
   let pe = Pcoq.Gram.Entry.parse 
 	     Pcoq.main_entry 
 	     (Pcoq.Gram.parsable (Stream.of_string s)) 
@@ -121,9 +122,10 @@ let try_interptac s =
     | _ ->
 	prerr_endline "try_interptac: not a tactic"; Failed
   with 
-  | Sys.Break -> prerr_endline "try_interp: interrupted"; Interrupted
-  | _ -> prerr_endline "try_interp: failed"; Failed
-	  
+  | Sys.Break | Stdpp.Exc_located (_,Sys.Break)
+      -> prerr_endline "try_interp: interrupted"; Interrupted
+  | Stdpp.Exc_located (_,e) -> prerr_endline ("try_interp: failed ("^(Printexc.to_string e)); Failed
+  | e -> Failed	  
 
 let is_tactic = function
   | VernacSolve _ -> true
@@ -204,6 +206,10 @@ let get_current_goals () =
     let sigma = Tacmach.evc_of_pftreestate pfts in
     List.map (prepare_goal sigma) gls
 
+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 
@@ -282,9 +288,6 @@ let reset_to_mod id =
 
 let hyp_menu (env, sigma, ((coqident,ident),_,ast),(s,pr_ast)) =
   [("Clear "^ident),("Clear "^ident^".");
-
-   ("Assumption"),
-   ("Assumption.");
    
    ("Apply "^ident),
    ("Apply "^ident^".");
@@ -335,7 +338,8 @@ let concl_menu (_,_,concl,_) =
     else 
       []) @
 
-  ["Omega", "Omega.";
+  ["Assumption" ,"Assumption.";
+   "Omega", "Omega.";
    "Ring", "Ring.";
    "Auto with *", "Auto with *.";
    "EAuto with *", "EAuto with *.";
@@ -350,7 +354,6 @@ let concl_menu (_,_,concl,_) =
    "Split", "Split.";
    "Left", "Left.";
    "Right", "Right.";
-
   ]
 
 
diff --git a/ide/coq.mli b/ide/coq.mli
index 9ab29eab0..3acc68683 100644
--- a/ide/coq.mli
+++ b/ide/coq.mli
@@ -30,6 +30,8 @@ type goal = hyp list * concl
 
 val get_current_goals : unit -> goal list
 
+val get_current_goals_nb : unit -> int
+
 val print_no_goal : unit -> string
 
 val process_exn : exn -> string*((int*int) option)
diff --git a/ide/coqide.ml b/ide/coqide.ml
index 719a8fcbe..dd975db27 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -119,7 +119,7 @@ type 'a viewable_script =
     }
 
 
-class type analyzed_views = 
+class type analyzed_views= 
 object('self)
     val mutable act_id : GtkSignal.id option
     val current_all : 'self viewable_script
@@ -234,33 +234,6 @@ let coq_computing = Mutex.create ()
 (* To prevent Coq from interrupting during undoing...*)
 let coq_may_stop = Mutex.create ()
 
-let full_do_if_not_computing f x = 
-  if Mutex.try_lock coq_computing then 
-    ignore (Thread.create 
-	      (async (fun () ->
-			prerr_endline "Launching thread";
-			let idle = 
-			  Glib.Timeout.add ~ms:300
-			    ~callback:(fun () -> !pulse ();true) in
-			begin
-			  prerr_endline "Getting lock";
-			  try
-			    f x;
-			    Glib.Timeout.remove idle;
-			    prerr_endline "Releasing lock";
-			    Mutex.unlock coq_computing;
-			  with e -> 
-			    Glib.Timeout.remove idle;
-			    prerr_endline "Releasing lock (on error)";
-			    Mutex.unlock coq_computing;
-			    raise e
-			end))
-	      ())
-  else prerr_endline "Discarded order (computations are ongoing)"
-
-let do_if_not_computing f x = 
-  ignore (full_do_if_not_computing f x)
-
 let break () = 
   if not (Mutex.try_lock coq_computing) then 
     begin
@@ -275,6 +248,48 @@ let break () =
     prerr_endline "Break received and discarded (not computing)"
   end
 
+let full_do_if_not_computing f x = 
+    ignore (Thread.create 
+	      (async (fun () ->
+			if Mutex.try_lock coq_computing then begin
+			  prerr_endline "Launching thread";
+			  let w = Blaster_window.blaster_window () in
+			  if not (Mutex.try_lock w#lock) then begin 
+			    break ();
+			    let lck = Mutex.create () in
+			    Mutex.lock lck;
+			    prerr_endline "Waiting on blaster...";
+			    Condition.wait w#blaster_killed lck;
+			    prerr_endline "Waiting on blaster ok";
+			    Mutex.unlock lck
+			  end else Mutex.unlock w#lock;
+			  let idle = 
+			      Glib.Timeout.add ~ms:300
+				~callback:(fun () -> !pulse ();true) in
+			    begin
+			      prerr_endline "Getting lock";
+			      try
+				f x;
+				Glib.Timeout.remove idle;
+			    prerr_endline "Releasing lock";
+			    Mutex.unlock w#lock;
+			    Mutex.unlock coq_computing;
+			      with e -> 
+				Glib.Timeout.remove idle;
+				prerr_endline "Releasing lock (on error)";
+				Mutex.unlock w#lock;
+				Mutex.unlock coq_computing;
+				raise e
+			    end
+			end else 
+			  prerr_endline 
+			    "Discarded order (computations are ongoing)"))
+	      ())
+
+let do_if_not_computing f x = 
+  ignore (full_do_if_not_computing f x)
+
+
 let add_input_view tv = 
   Vector.append input_views tv
 
@@ -1050,7 +1065,9 @@ object(self)
 	false
 
   method process_until_iter_or_error stop =
+    let stop' = `OFFSET stop#offset in
     let start = self#get_start_of_input#copy in
+    let start' = `OFFSET start#offset in
     input_buffer#apply_tag_by_name 
       ~start
       ~stop
@@ -1065,6 +1082,9 @@ object(self)
      with Sys.Break -> 
        prerr_endline "Interrupted during process_until_iter_or_error");
     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()
@@ -1226,30 +1246,55 @@ Please restart and report NOW.";
     else prerr_endline "undo_last_step discarded"
 
       
-  method blaster () =
-    prerr_endline "Blaster called";
-    let c = Blaster_window.blaster_window () in
-    c#clear ();
-    let set i s = 
-      c#set
-	i
-	s 
-	(fun () -> try_interptac (s ^ ". "))
-	(fun () -> self#insert_command (s^".\n") (s^".\n"))
-    in
-    set "Goal" "Assumption" ;
-    set "Goal" "Reflexivity" ;
-    set "Goal" "Trivial";
-    set "Goal" "Auto" ;
-    set "Goal" "EAuto";
-    set "Goal" "Auto with *" ;
-    set "Goal" "EAuto with *" ;
-    set "Goal" "Intuition";
-    set "Goal" "Ground";
-    let _ = Thread.create c#blaster () in
-    ()
-    
+  method blaster () = 
     
+    ignore (Thread.create 
+	      (fun () ->  
+		 prerr_endline "Blaster called";
+		 let c = Blaster_window.present_blaster_window () in
+		 if Mutex.try_lock c#lock then begin
+		   c#clear ();
+		   let current_gls = try get_current_goals () with _ -> [] in
+		   let gls_nb = List.length current_gls in
+		   
+		   let set_goal i (s,t) = 
+		     let gnb = string_of_int i in
+		     let s = gnb ^":"^s in
+		     let t' = gnb ^": Progress "^t in
+		     let t'' = gnb ^": "^t in
+		     c#set
+		       ("Goal "^gnb)
+		       s 
+		       (fun () -> try_interptac t')
+		       (fun () -> self#insert_command t'' t'')
+		   in
+		   let set_current_goal (s,t) = 
+		     c#set
+		       "Goal 1"
+		       s 
+		       (fun () -> try_interptac ("Progress "^t))
+		       (fun () -> self#insert_command t t)
+		   in
+		   begin match current_gls with 
+		   | [] -> ()
+		   | (hyp_l,current_gl)::r ->
+		       List.iter set_current_goal (concl_menu current_gl);
+		       List.iter 
+			 (fun hyp -> 
+			    List.iter set_current_goal (hyp_menu hyp))
+			 hyp_l;
+		       let i = ref 2 in
+		       List.iter 
+			 (fun (hyp_l,gl) -> 
+			    List.iter (set_goal !i) (concl_menu gl);
+			    incr i)
+			 r
+		   end;
+		   let _ =  c#blaster () in
+		   Mutex.unlock c#lock
+		 end else prerr_endline "Blaster discarded")
+	      ())
+      
   method insert_command cp ip = 
     self#clear_message;
     ignore (self#insert_this_phrase_on_success true false false cp ip)
@@ -1908,7 +1953,8 @@ let main files =
     else
       begin
 	!flash_info "New proof started";
-	activate_input (notebook ())#current_page
+	activate_input (notebook ())#current_page;
+	ignore (f analyzed_view)
       end
   in
 
@@ -1973,16 +2019,17 @@ let main files =
       ~accel_group 
       ~accel_modi:!current.modifier_for_tactics
   in
-  let do_if_active f () = 
+  let do_if_active_raw f () = 
     let current = get_current_view () in
     let analyzed_view = out_some current.analyzed_view in
     if analyzed_view#is_active then ignore (f analyzed_view)
   in
-  let do_if_active f = do_if_not_computing (do_if_active f) in
+  let do_if_active f = do_if_not_computing (do_if_active_raw f) in
 
   ignore (tactics_factory#add_item "_Blaster"
 	    ~key:GdkKeysyms._b
-	    ~callback:(do_if_active (fun a -> a#blaster ()))
+	    ~callback: (do_if_active_raw (fun a -> a#blaster ()))
+	    (* Custom locking mechanism! *)
 	 )
 	 ;