Ajout des options Coqide suggérées par Damien Doligez (wish #1053)

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

4 files changed, 54 insertions, 19 deletions

diff --git a/ide/coqide.ml b/ide/coqide.ml
index 849479e53..0b5daaffb 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -1224,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
diff --git a/ide/find_phrase.mll b/ide/find_phrase.mll
index 1e608bf75..677ca428f 100644
--- a/ide/find_phrase.mll
+++ b/ide/find_phrase.mll
@@ -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/preferences.ml b/ide/preferences.ml
index 843c98aec..1dfa69980 100644
--- a/ide/preferences.ml
+++ b/ide/preferences.ml
@@ -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 {
@@ -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 50b988e90..7d2be0012 100644
--- a/ide/preferences.mli
+++ b/ide/preferences.mli
@@ -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