coqide: .* on start/add \n on eof

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

4 files changed, 26 insertions, 5 deletions

diff --git a/Makefile b/Makefile
index 36545e5bda..cc7bfe1dc9 100644
--- a/Makefile
+++ b/Makefile
@@ -400,7 +400,7 @@ beforedepend:: ide/config_parser.mli ide/config_parser.ml
 beforedepend:: ide/utf8_convert.ml
 
 FULLIDELIB=$(FULLCOQLIB)/ide
-IDEFILES=ide/coq.png ide/.coqide-gtk2rc
+IDEFILES=ide/coq.png ide/.coqide-gtk2rc ide/FAQ
 
 ide: $(COQIDEBYTE) $(COQIDE) states
 clean-ide: 
diff --git a/ide/coqide.ml b/ide/coqide.ml
index 85e412df63..db0f394e6e 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -732,7 +732,7 @@ object(self)
       with e -> prerr_endline ("Don't worry be happy despite: "^Printexc.to_string e)
 	
 
-  val mutable full_goal_done = false
+  val mutable full_goal_done = true
 
   method show_goals_full = 
     if not full_goal_done then
@@ -910,7 +910,16 @@ object(self)
       in
       end_iter#nocopy#set_offset (start#offset + !Find_phrase.length);
       Some (start,end_iter)
-    with _ -> None
+    with
+    | Find_phrase.EOF s -> 
+	(* Phrase is at the end of the buffer*)
+	let si = start#offset in
+	let ei = si + !Find_phrase.length in
+	end_iter#nocopy#set_offset (ei - 1);
+	input_buffer#insert ~iter:end_iter "\n";
+	Some (input_buffer#get_iter (`OFFSET si),
+	      input_buffer#get_iter (`OFFSET ei))
+    | _ -> None
 
   method complete_at_offset (offset:int) = 
     prerr_endline ("Completion at offset : " ^ string_of_int offset);
@@ -2267,6 +2276,8 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S);
 				    match get_current_view () with  
 				    | {view=v;analyzed_view=Some av} -> 
 			      		let w = GWindow.window ~show:true 
+						  ~width:(!current.window_width/2)
+						  ~height:(!current.window_height)
 						  ~title:(match av#filename with
 							  | None -> "*Unamed*"
 							  | Some f -> f) 
@@ -2280,6 +2291,8 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S);
 						   ~packing:sb#add 
 						   ()
 					in
+					nv#misc#modify_font 
+					  !current.text_font; 
 					ignore (w#connect#destroy 
 						  ~callback:
 						  (fun () -> av#remove_detached_view w));
@@ -2593,7 +2606,7 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S);
 		   old_h := h;
 		   old_w := w;
 		   hb#set_position (w/2);
-		   hb2#set_position (h*4/5);
+		   hb2#set_position (h/2);
 		   !current.window_height <- h;
 		   !current.window_width <- w;
 		 end
diff --git a/ide/find_phrase.mll b/ide/find_phrase.mll
index 94fc0174fa..6f13e72e24 100644
--- a/ide/find_phrase.mll
+++ b/ide/find_phrase.mll
@@ -12,6 +12,8 @@
   exception Lex_error of string
   let length = ref 0
   let buff = Buffer.create 513
+  exception EOF of string
+
 }
 
 let phrase_sep = '.'
@@ -30,6 +32,12 @@ rule next_phrase = parse
       length := !length + 2; 
       Buffer.add_string buff (Lexing.lexeme lexbuf);
       Buffer.contents buff}
+
+  | phrase_sep eof{
+      length := !length + 2; 
+      Buffer.add_string buff (Lexing.lexeme lexbuf);
+      Buffer.add_char buff '\n';
+      raise (EOF(Buffer.contents buff))}
   | _ 
       { 
 	let c = Lexing.lexeme_char lexbuf 0 in 
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 7cc7a67e0f..d67dd0dfdc 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -215,7 +215,7 @@ let parse_args is_ide =
        parse rem
 
     | s :: rem -> 
-	if is_ide && Filename.check_suffix s ".v" then begin
+	if is_ide then begin
 	  ide_args := s :: !ide_args;
 	  parse rem
 	end else begin