coqide: blaster V1

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

7 files changed, 160 insertions, 79 deletions

diff --git a/.depend b/.depend
index 4f29c8452c..2d49a1212f 100644
--- a/.depend
+++ b/.depend
@@ -476,6 +476,8 @@ dev/top_printers.cmx: parsing/ast.cmx toplevel/cerrors.cmx proofs/clenv.cmx \
     kernel/term.cmx pretyping/termops.cmx kernel/univ.cmx 
 doc/parse.cmo: parsing/ast.cmi 
 doc/parse.cmx: parsing/ast.cmx 
+ide/blaster_window.cmo: ide/coq.cmi 
+ide/blaster_window.cmx: ide/coq.cmx 
 ide/command_windows.cmo: ide/coq.cmi ide/coq_commands.cmo ide/ideutils.cmi \
     ide/command_windows.cmi 
 ide/command_windows.cmx: ide/coq.cmx ide/coq_commands.cmx ide/ideutils.cmx \
@@ -491,9 +493,9 @@ ide/coq.cmo: toplevel/cerrors.cmi config/coq_config.cmi toplevel/coqtop.cmi \
     library/nametab.cmi lib/options.cmi parsing/pcoq.cmi proofs/pfedit.cmi \
     lib/pp.cmi parsing/printer.cmi proofs/proof_trees.cmi \
     pretyping/reductionops.cmi proofs/refiner.cmi library/states.cmi \
-    proofs/tacmach.cmi tactics/tactics.cmi kernel/term.cmi lib/util.cmi \
-    toplevel/vernac.cmi toplevel/vernacentries.cmi toplevel/vernacexpr.cmo \
-    ide/coq.cmi 
+    tactics/tacinterp.cmi proofs/tacmach.cmi tactics/tactics.cmi \
+    kernel/term.cmi lib/util.cmi toplevel/vernac.cmi \
+    toplevel/vernacentries.cmi toplevel/vernacexpr.cmo ide/coq.cmi 
 ide/coq.cmx: toplevel/cerrors.cmx config/coq_config.cmx toplevel/coqtop.cmx \
     kernel/declarations.cmx kernel/environ.cmx pretyping/evarutil.cmx \
     pretyping/evd.cmx library/global.cmx tactics/hipattern.cmx \
@@ -501,19 +503,19 @@ ide/coq.cmx: toplevel/cerrors.cmx config/coq_config.cmx toplevel/coqtop.cmx \
     library/nametab.cmx lib/options.cmx parsing/pcoq.cmx proofs/pfedit.cmx \
     lib/pp.cmx parsing/printer.cmx proofs/proof_trees.cmx \
     pretyping/reductionops.cmx proofs/refiner.cmx library/states.cmx \
-    proofs/tacmach.cmx tactics/tactics.cmx kernel/term.cmx lib/util.cmx \
-    toplevel/vernac.cmx toplevel/vernacentries.cmx toplevel/vernacexpr.cmx \
-    ide/coq.cmi 
+    tactics/tacinterp.cmx proofs/tacmach.cmx tactics/tactics.cmx \
+    kernel/term.cmx lib/util.cmx toplevel/vernac.cmx \
+    toplevel/vernacentries.cmx toplevel/vernacexpr.cmx ide/coq.cmi 
 ide/coq_tactics.cmo: ide/coq_tactics.cmi 
 ide/coq_tactics.cmx: ide/coq_tactics.cmi 
-ide/coqide.cmo: ide/command_windows.cmi ide/coq.cmi ide/coq_commands.cmo \
-    ide/find_phrase.cmo ide/highlight.cmo ide/ideutils.cmi proofs/pfedit.cmi \
-    ide/preferences.cmi ide/undo.cmi lib/util.cmi toplevel/vernacexpr.cmo \
-    ide/coqide.cmi 
-ide/coqide.cmx: ide/command_windows.cmx ide/coq.cmx ide/coq_commands.cmx \
-    ide/find_phrase.cmx ide/highlight.cmx ide/ideutils.cmx proofs/pfedit.cmx \
-    ide/preferences.cmx ide/undo.cmx lib/util.cmx toplevel/vernacexpr.cmx \
-    ide/coqide.cmi 
+ide/coqide.cmo: ide/blaster_window.cmo ide/command_windows.cmi ide/coq.cmi \
+    ide/coq_commands.cmo ide/find_phrase.cmo ide/highlight.cmo \
+    ide/ideutils.cmi proofs/pfedit.cmi ide/preferences.cmi ide/undo.cmi \
+    lib/util.cmi toplevel/vernacexpr.cmo ide/coqide.cmi 
+ide/coqide.cmx: ide/blaster_window.cmx ide/command_windows.cmx ide/coq.cmx \
+    ide/coq_commands.cmx ide/find_phrase.cmx ide/highlight.cmx \
+    ide/ideutils.cmx proofs/pfedit.cmx ide/preferences.cmx ide/undo.cmx \
+    lib/util.cmx toplevel/vernacexpr.cmx ide/coqide.cmi 
 ide/find_phrase.cmo: ide/ideutils.cmi 
 ide/find_phrase.cmx: ide/ideutils.cmx 
 ide/highlight.cmo: ide/ideutils.cmi 
diff --git a/Makefile b/Makefile
index e4fb19ef65..54cce58539 100644
--- a/Makefile
+++ b/Makefile
@@ -386,7 +386,7 @@ COQIDE=bin/coqide$(EXE)
 COQIDECMO=ide/utils/okey.cmo ide/utils/uoptions.cmo \
 	  ide/utils/configwin_keys.cmo ide/utils/configwin_types.cmo \
 	  ide/utils/configwin_messages.cmo ide/utils/configwin_ihm.cmo \
-	  ide/utils/configwin.cmo \
+	  ide/utils/configwin.cmo ide/blaster_window.cmo \
 	  ide/utils/editable_cells.cmo ide/config_parser.cmo \
 	  ide/config_lexer.cmo ide/utf8_convert.cmo ide/preferences.cmo \
 	  ide/ideutils.cmo ide/undo.cmo \
diff --git a/ide/coq.ml b/ide/coq.ml
index 8351149329..2df19fd776 100644
--- a/ide/coq.ml
+++ b/ide/coq.ml
@@ -96,6 +96,35 @@ let interp s =
 	      last
 	  | None -> assert false
 
+let nb_subgoals pf =
+  List.length (fst (Refiner.frontier (Tacmach.proof_of_pftreestate pf)))
+
+type tried_tactic = 
+  | Interrupted
+  | Success of int (* nb of goals after *)
+  | Failed
+
+let try_interptac s = 
+  try
+    prerr_endline ("Starting try_interptac: "^s);
+    let pf = get_pftreestate () in
+    let pe = Pcoq.Gram.Entry.parse 
+	       Pcoq.main_entry 
+	       (Pcoq.Gram.parsable (Stream.of_string s)) 
+    in match pe with 
+    | Some (loc,(VernacSolve (n, tac, _))) ->
+	let tac = Tacinterp.interp tac in
+	let pf' = solve_nth_pftreestate n tac pf in
+	prerr_endline "Success";
+	let nb_goals = nb_subgoals pf' - nb_subgoals pf in
+	Success nb_goals
+    | _ ->
+	prerr_endline "try_interptac: not a tactic"; Failed
+  with 
+  | Sys.Break -> prerr_endline "try_interp: interrupted"; Interrupted
+  | _ -> prerr_endline "try_interp: failed"; Failed
+	  
+
 let is_tactic = function
   | VernacSolve _ -> true
   | _ -> false
diff --git a/ide/coq.mli b/ide/coq.mli
index 7769a037b9..9ab29eab0b 100644
--- a/ide/coq.mli
+++ b/ide/coq.mli
@@ -48,3 +48,11 @@ val is_in_coq_lib : string -> bool
 
 val make_cases : string -> string list list
 
+
+type tried_tactic = 
+  | Interrupted
+  | Success of int (* nb of goals after *)
+  | Failed
+
+val try_interptac: string -> tried_tactic
+
diff --git a/ide/coqide.ml b/ide/coqide.ml
index 6a9a202e82..6d96fc3008 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -186,7 +186,9 @@ object('self)
     method undo_last_step : unit
     method help_for_keyword : unit -> unit
     method complete_at_offset : int -> unit
-  end
+
+    method blaster : unit -> unit
+end
 
 let (input_views:analyzed_views viewable_script Vector.t) = Vector.create ()
 
@@ -309,29 +311,29 @@ let remove_current_view_page () =
   ((notebook ())#get_nth_page c)#misc#hide ()
 
 let underscore = Glib.Utf8.to_unichar "_" (ref 0)
+let bn = Glib.Utf8.to_unichar "\n" (ref 0)
+
+let starts_word it = it#starts_word && it#backward_char#char <> underscore
+let ends_word it = it#ends_line || (it#ends_word && it#char <> underscore)
+let inside_word it = it#inside_word || it#char = underscore || it#backward_char#char = underscore
+let is_on_word_limit it = inside_word it || ends_word it 
 
-let rec find_word_end it =
-  prerr_endline "Find word end";
-  if 
-    (it#ends_word && 
-    it#char <> underscore)
-    || it#forward_char#is_end
-  then it 
-  else find_word_end it#forward_word_end
-      
 let rec find_word_start it =
   prerr_endline "Find word start";
-  if 
-    (it#starts_word && 
-    it#backward_char#char <> underscore)
-    || it#backward_char#is_start
-  then it 
-  else find_word_start it#backward_word_start
-
-let get_last_word_limits it = 
+  if starts_word it
+  then it
+  else find_word_start it#backward_char
+
+let rec find_word_end it =
+  prerr_endline "Find word end";
+  if ends_word it
+  then it
+  else find_word_end it#forward_char
+
+let get_word_around it = 
   let start = find_word_start it in
-  let nw = start#backward_word_start in
-  (find_word_start nw,find_word_end nw)
+  let stop =  find_word_end it in
+  start,stop
 
 
 let rec complete_backward w (it:GText.iter) = 
@@ -339,21 +341,24 @@ let rec complete_backward w (it:GText.iter) =
 	  match it#backward_search w with 
 	    | None -> None
 	    | Some (start,stop) -> 
-		let ne = find_word_end stop in
-		if ((find_word_start start)#compare start <> 0) ||
-		  (ne#compare stop = 0)
-		then complete_backward w start
-		else Some (stop,ne)
+		if starts_word start then 
+		  let ne = find_word_end stop in
+		  if ne#compare stop = 0
+		  then complete_backward w start
+		  else Some (start,stop,ne)
+		else complete_backward w start
 		  
 let rec complete_forward w (it:GText.iter) = 
   prerr_endline "Complete forward...";
   match it#forward_search w with 
     | None -> None
-    | Some (start,stop) -> let ne = find_word_end stop in
-      if ((find_word_start start)#compare start <> 0) || 
-	ne#compare stop = 0 then complete_forward w stop
-      else Some (stop,ne)
-
+    | Some (start,stop) -> 
+	if starts_word start then 	
+	  let ne = find_word_end stop in
+	  if ne#compare stop = 0 then 
+	    complete_forward w stop
+	  else Some (stop,stop,ne)
+	else complete_forward w stop
 
 (* Reset this to None on page change ! *)
 let (last_completion:(string*int*int*bool) option ref) = ref None
@@ -361,7 +366,7 @@ let (last_completion:(string*int*int*bool) option ref) = ref None
 let () = to_do_on_page_switch := 
 	 (fun i -> last_completion := None)::!to_do_on_page_switch
 
-let complete input_buffer w (offset:int) =
+let rec complete input_buffer w (offset:int) =
   match !last_completion with 
     | Some (lw,loffset,lpos,backward)
 	when lw=w && loffset=offset ->
@@ -372,30 +377,31 @@ let complete input_buffer w (offset:int) =
 	      | None -> 
 		  last_completion := 
 		Some (lw,loffset,
-		      
-		      (input_buffer#get_iter (`OFFSET loffset))#
-		      forward_word_end#offset ,
+		      (find_word_end (input_buffer#get_iter (`OFFSET loffset)))#offset ,
 		      false); 
 		  None
-	      | Some (start,stop) as result -> 
+	      | Some (ss,start,stop) as result -> 
 		  last_completion := 
-		Some (w,offset,start#backward_char#offset,true);
+		Some (w,offset,ss#offset,true);
 		  result
 	  else
 	    match complete_forward w iter with
 	      | None -> 
 		  last_completion := None;
 		  None
-	      | Some (start,stop) as result -> 
+	      | Some (ss,start,stop) as result -> 
 		  last_completion := 
-		Some (w,offset,start#forward_char#offset,false);
+		Some (w,offset,ss#offset,false);
 		  result
 	end
     | _ -> begin
 	match complete_backward w (input_buffer#get_iter (`OFFSET offset)) with
-	  | None -> last_completion := None; None
-	  | Some (start,stop) as result -> 
-	      last_completion := Some (w,offset,start#offset,true);
+	  | None -> 
+	      last_completion := 
+	    Some (w,offset,(find_word_end (input_buffer#get_iter (`OFFSET offset)))#offset,false);
+	      complete input_buffer w offset
+	  | Some (ss,start,stop) as result -> 
+	      last_completion := Some (w,offset,ss#offset,true);
 	      result
       end
 	  
@@ -921,20 +927,21 @@ object(self)
     prerr_endline ("Completion at offset : " ^ string_of_int offset);
     let it () = input_buffer#get_iter (`OFFSET offset) in
     let iit = it () in
-    if (iit#ends_word || iit#inside_word) then 
+    let start = find_word_start iit in
+    if is_on_word_limit iit then 
       let w = input_buffer#get_text 
-		~start:(find_word_start iit)
+		~start
 		~stop:iit
 		()
       in
       prerr_endline ("Completion of prefix : " ^ w);
-      match complete input_buffer w offset with 
+      match complete input_buffer w start#offset with 
       | None -> () 
-      | Some (start,stop) -> 
+      | Some (ss,start,stop) -> 
 	  let completion = input_buffer#get_text ~start ~stop () in
 	  ignore (input_buffer#delete_selection ());
 	  ignore (input_buffer#insert_interactive completion);
-	  input_buffer#move_mark `INSERT (it());
+	  input_buffer#move_mark `SEL_BOUND (it())#backward_char;
 	  ()
 	  
   method process_next_phrase display_goals do_highlight = 
@@ -1218,6 +1225,29 @@ Please restart and report NOW.";
        Mutex.unlock coq_may_stop)
     else prerr_endline "undo_last_step discarded"
 
+      
+  method blaster () = 
+    prerr_endline "Blaster called";
+    let c = Blaster_window.blaster_window () in
+    let set i s = 
+      c#set i
+	s 
+	(fun () -> try_interptac (s ^ ". "))
+	(fun () -> prerr_endline "Clicked")
+    in
+    set 0 "Assumption" ;
+    set 1 "Reflexivity" ;
+    set 2 "Trivial";
+    set 3 "Auto" ;
+    set 4 "EAuto";
+    set 5 "Auto with *" ;
+    set 6 "EAuto with *" ;
+    set 7 "Intuition";
+    set 8 "Ground";
+    let _ = Thread.create c#blaster () in
+    ()
+    
+    
   method insert_command cp ip = 
     self#clear_message;
     ignore (self#insert_this_phrase_on_success true false false cp ip)
@@ -1719,8 +1749,8 @@ let main files =
 	  !current.cmd_coqdoc ^ " -ps " ^ Filename.basename f ^ 
 	  " | " ^ !current.cmd_print
 	in
-	let c = Sys.command cmd in
-	!flash_info (cmd ^ if c = 0 then " succeeded" else " failed")
+	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
 
@@ -1744,8 +1774,11 @@ let main files =
 	  "cd " ^ Filename.dirname f ^ "; " ^
 	  !current.cmd_coqdoc ^ " --" ^ kind ^ " -o " ^ output ^ " " ^ basef
 	in
-	let c = Sys.command cmd in
-	!flash_info (cmd ^ if c = 0 then " succeeded" else " failed")
+	let s,_ = run_command av#insert_message cmd in
+	!flash_info (cmd ^ 
+		     if s = Unix.WEXITED 0 
+		     then " succeeded" 
+		     else " failed")
   in
   let file_export_m =  file_factory#add_submenu "E_xport to" in
 
@@ -1827,13 +1860,11 @@ let main files =
 		 with _ -> prerr_endline "EMIT PASTE FAILED")));
   ignore (edit_f#add_separator ());
   let read_only_i = edit_f#add_check_item "Expert" ~active:false
-		      (* ~key:GdkKeysyms._Z *)
-		      ~callback:(fun b -> 
-				   (* GtkData.AccelMap.save "test.accel" *) 
-				   ()
-				) 
+		      ~key:GdkKeysyms._B
+		      ~callback:(fun b -> ()
+				)
   in
-  read_only_i#misc#set_state `INSENSITIVE;
+(*  read_only_i#misc#set_state `INSENSITIVE;*)
 
   let search_if = edit_f#add_item "Search _forward"
 		    ~key:GdkKeysyms._greater
@@ -1846,8 +1877,9 @@ let main files =
 		     ~callback:
 		     (do_if_not_computing 
 			(fun b -> 
-			   let v =out_some (get_current_view ()).analyzed_view 
-			   in v#complete_at_offset (v#get_insert#offset)
+			   let v = out_some (get_current_view ()).analyzed_view 
+				    
+			   in v#complete_at_offset ((v#view#buffer#get_iter `SEL_BOUND)#offset)
 			))
   in
 
@@ -1945,6 +1977,12 @@ let main files =
     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
+  ignore (tactics_factory#add_item "_Blaster" 
+	    ~key:GdkKeysyms._b
+	    ~callback:(do_if_active (fun a -> a#blaster ()))
+	 )
+	 ;
+
   ignore (tactics_factory#add_item "_Auto" 
 	    ~key:GdkKeysyms._a
 	    ~callback:(do_if_active (fun a -> a#insert_command "Progress Auto.\n" "Auto.\n"))
@@ -2204,9 +2242,11 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S);
   
   (* Command/CoqMakefile Menu*)
   let coq_makefile_f () =
-    let c = Sys.command !current.cmd_coqmakefile in
+    let v = get_active_view () in
+    let av = out_some v.analyzed_view in
+    let s,res = run_command av#insert_message !current.cmd_coqmakefile in
     !flash_info 
-      (!current.cmd_coqmakefile ^ if c = 0 then " succeeded" else " failed")
+      (!current.cmd_coqmakefile ^ if s = Unix.WEXITED 0 then " succeeded" else " failed")
   in
   let _ = externals_factory#add_item "_Make Makefile" ~callback:coq_makefile_f 
   in
@@ -2650,6 +2690,7 @@ let start () =
 						      `WARNING;`CRITICAL]
     (fun ~level msg -> failwith ("Coqide internal error: " ^ msg));
   Command_windows.main ();
+  Blaster_window.main 9;
   main files;
   while true do 
     try 
diff --git a/ide/ideutils.ml b/ide/ideutils.ml
index 4cf9c1ba22..f8af156c47 100644
--- a/ide/ideutils.ml
+++ b/ide/ideutils.ml
@@ -244,7 +244,7 @@ let rec print_list print fmt = function
 
 let run_command f c =
   let result = Buffer.create 127 in
-  let cin,cout,cerr = Unix.open_process_full c [||] in
+  let cin,cout,cerr = Unix.open_process_full c (Unix.environment ()) in
   let buff = String.make 127 ' ' in
   let buffe = String.make 127 ' ' in
   let n = ref 0 in
@@ -253,10 +253,10 @@ let run_command f c =
   while n:= input cin buff 0 127 ; ne := input cerr buffe 0 127 ; 
     !n+ !ne <> 0
   do 
-    let r = String.sub buff 0 !n in 
+    let r = try_convert (String.sub buff 0 !n) in 
     f r;
     Buffer.add_string result r;
-    let r = String.sub buffe 0 !ne in 
+    let r = try_convert (String.sub buffe 0 !ne) in 
     f r;
     Buffer.add_string result r 
   done;
diff --git a/ide/undo.ml b/ide/undo.ml
index 10d5e0ab50..5099580667 100644
--- a/ide/undo.ml
+++ b/ide/undo.ml
@@ -1,3 +1,4 @@
+
 (***********************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
 (* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
@@ -27,7 +28,7 @@ object(self)
   val nredo = (Stack.create () : action Stack.t)
 
   method private dump_debug =
-    if !debug then begin
+    if false (* !debug *) then begin
       prerr_endline "==========Stack top=============";
       Stack.iter 
 	(fun e -> match e with