coqide: corrections pour utf8 de coq. highlight synchrone=repare le bug autorepeat des paste. configuration des accel rateurs. les chaines peuvent contenir des points. Bug: les phrases ne peuvent pas contenir .\sep. Or c'est permis par les Notation.

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

10 files changed, 247 insertions, 65 deletions

diff --git a/ide/coqide.ml b/ide/coqide.ml
index c3f92d609b..15b34b8dca 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -593,7 +593,7 @@ object(self)
 	 if localize then 
 	   (match loc with 
 	      | None -> ()
-	      | Some (start,stop) -> 
+	      | 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
@@ -1006,7 +1006,7 @@ object(self)
 	    else set_tab_image index yes_icon;
 	 ));
     ignore (input_view#connect#after#paste_clipboard
-	      ~callback:(fun () ->
+	      ~callback:(fun () -> 
 			   prerr_endline "Paste occured"));
     ignore (input_buffer#connect#changed
 	      ~callback:(fun () -> 
@@ -1088,6 +1088,10 @@ let create_input_tab filename =
   tv1
  
 let main files = 
+  (* Statup preferences *)
+  load_pref current;
+
+  (* Main window *)
   let w = GWindow.window 
 	    ~allow_grow:true ~allow_shrink:true 
 	    ~width:window_width ~height:window_height 
@@ -1138,9 +1142,10 @@ let main files =
       input_buffer#place_cursor input_buffer#start_iter;
       set_current_view index;
       Highlight.highlight_all input_buffer;
-      input_buffer#set_modified false
+      input_buffer#set_modified false;
+      av#view#clear_undo
     with       
-      | Vector.Found i -> !flash_info "File already opened"
+      | Vector.Found i -> set_current_view i
       | e -> !flash_info "Load failed"
   in
   let load_m = file_factory#add_item "_Open/Create" ~key:GdkKeysyms._O in
@@ -1358,7 +1363,7 @@ let main files =
 	      ignore (get_current_view()).view#undo));
   ignore(edit_f#add_item "_Clear Undo Stack" ~key:GdkKeysyms._exclam ~callback:
 	   (fun () -> 
-	      ignore (get_current_view()).view#undo));
+	      ignore (get_current_view()).view#clear_undo));
   ignore(edit_f#add_separator ());
   ignore(edit_f#add_item "Copy" ~key:GdkKeysyms._C ~callback:
 	   (fun () -> GtkSignal.emit_unit
@@ -1433,11 +1438,11 @@ let main files =
 	 );
 
   (* Tactics Menu *)
-  let tactics_menu =  factory#add_submenu "T_actics" in
+  let tactics_menu =  factory#add_submenu "_Try Tactics" in
   let tactics_factory = 
     new GMenu.factory tactics_menu 
       ~accel_group 
-      ~accel_modi:current.modifier_for_templates 
+      ~accel_modi:current.modifier_for_tactics
   in
   let do_if_active f () = 
     let current = get_current_view () in
@@ -1627,7 +1632,8 @@ let main files =
       revert_timer := Some
 	(GMain.Timeout.add ~ms:current.global_auto_revert_delay 
 	   ~callback:(fun () -> revert_f ();true))
-  in
+  in reset_revert_timer (); (* to enable statup preferences timer *)
+
   let configuration_menu = factory#add_submenu "Confi_guration" in
   let configuration_factory = new GMenu.factory configuration_menu ~accel_group
   in
@@ -1683,10 +1689,6 @@ let main files =
   let _ = help_factory#add_separator () in
   let about_m = help_factory#add_item "_About" in
 
-  (* Statup preferences *)
-  load_pref current;
-  reset_revert_timer ();
-
   (* Window layout *)
 
   let hb = GPack.paned `HORIZONTAL  ~border_width:3 ~packing:vbox#add () in
@@ -1830,7 +1832,7 @@ let start () =
   with Not_found -> ());
   ignore (GtkMain.Main.init ());
   GtkData.AccelGroup.set_default_mod_mask 
-    (Some [`CONTROL;`SHIFT;`MOD1;`MOD2;`MOD3;`MOD4;`MOD5;`LOCK]);
+    (Some [`CONTROL;`SHIFT;`MOD1;`MOD4]);
   cb_ := Some (GtkBase.Clipboard.get Gdk.Atom.primary);
   Glib.Message.set_log_handler ~domain:"Gtk" ~levels:[`ERROR;`FLAG_FATAL;
 						      `WARNING;`CRITICAL]
@@ -1846,6 +1848,7 @@ let start () =
     with 
       | Sys.Break -> prerr_endline "Interrupted." ; flush stderr
       | e -> 
-	  prerr_endline ("CoqIde fatal error:" ^ (Printexc.to_string e));
+	  Pervasives.prerr_endline ("CoqIde unexpected error:" ^ (Printexc.to_string e));
+	  flush stderr;
 	  crash_save 127
   done
diff --git a/ide/find_phrase.mll b/ide/find_phrase.mll
index 8a428710ac..16d1cd83ef 100644
--- a/ide/find_phrase.mll
+++ b/ide/find_phrase.mll
@@ -8,6 +8,12 @@ rule next_phrase = parse
   | "(*" { incr length; incr length; 
 	   skip_comment lexbuf;
 	   next_phrase lexbuf}
+  | '"'[^'"']*'"' { let lexeme = Lexing.lexeme lexbuf in 
+		 let ulen = Glib.Utf8.length lexeme in
+		 length := !length + ulen;
+		 Buffer.add_string buff lexeme;
+		 next_phrase lexbuf
+	       }
   | '.'[' ''\n''\t''\r'] {	
       length := !length + 2; 
       Buffer.add_string buff (Lexing.lexeme lexbuf);
@@ -19,7 +25,7 @@ rule next_phrase = parse
 	Buffer.add_char buff c ;
 	next_phrase lexbuf
       }
-  | eof  { raise (Lex_error "no phrase") }
+  | eof  { raise (Lex_error "Phrase should end with . followed by a separator") }
 and skip_comment = parse
   | "*)" {incr length; incr length; ()}
   | "(*" {incr length; incr length; 
diff --git a/ide/highlight.mll b/ide/highlight.mll
index b50ea148ee..2e8ce66596 100644
--- a/ide/highlight.mll
+++ b/ide/highlight.mll
@@ -73,7 +73,7 @@ and comment = parse
 	let lb = Lexing.from_string s in
 	try 
 	  while true do
-	    process_pending ();
+	    (* process_pending (); This is VERY DANGEROUS *)
 	    let b,e,o=next_order lb in
 	    let b,e = convert_pos b,convert_pos e in
 	    let start = input_buffer#get_iter_at_char (offset + b) in
diff --git a/ide/ideutils.ml b/ide/ideutils.ml
index 20a06ae12e..6373e5a344 100644
--- a/ide/ideutils.ml
+++ b/ide/ideutils.ml
@@ -10,14 +10,22 @@ let get_insert input_buffer = input_buffer#get_iter_at_mark `INSERT
 let is_char_start c = let code = Char.code c in code < 0x80 || code >= 0xc0
 
 let byte_offset_to_char_offset s byte_offset = 
-  assert (byte_offset < String.length s);
-  let count_delta = ref 0 in
-  for i = 0 to byte_offset do
-    let code = Char.code s.[i] in
-    if code >= 0x80 && code < 0xc0 then incr count_delta
-  done;
-  byte_offset - !count_delta
-
+  if (byte_offset < String.length s) then begin
+    let count_delta = ref 0 in
+    for i = 0 to byte_offset do
+      let code = Char.code s.[i] in
+      if code >= 0x80 && code < 0xc0 then incr count_delta
+    done;
+    byte_offset - !count_delta
+  end
+  else begin
+    let count_delta = ref 0 in
+    for i = 0 to String.length s - 1 do
+      let code = Char.code s.[i] in
+      if code >= 0x80 && code < 0xc0 then incr count_delta
+    done;
+    byte_offset - !count_delta
+  end
 
 let process_pending () =
   while Glib.Main.pending () do 
@@ -50,7 +58,7 @@ let try_export file_name s =
       if (fst (Glib.Convert.get_charset ())) then
 	s 
       else
-	Glib.Convert.locale_from_utf8 s 
+	(try Glib.Convert.locale_from_utf8 s with _ -> prerr_endline "Warning: exporting to utf8";s)
     in
     let oc = open_out file_name in
     output_string oc s;
diff --git a/ide/preferences.ml b/ide/preferences.ml
index 398d0ef59f..bbd1d062b2 100644
--- a/ide/preferences.ml
+++ b/ide/preferences.ml
@@ -57,7 +57,9 @@ type pref =
 
       mutable modifier_for_navigation : Gdk.Tags.modifier list;
       mutable modifier_for_templates : Gdk.Tags.modifier list;
-      
+      mutable modifier_for_tactics : Gdk.Tags.modifier list;
+      mutable modifiers_valid : Gdk.Tags.modifier list;
+
       mutable cmd_browse : string * string;
 
       mutable doc_url : string;
@@ -104,6 +106,15 @@ let save_pref p =
       "modifier_for_templates" 
       output_modi 
       p.modifier_for_templates;
+    output_list 
+      "modifier_for_tactics" 
+      output_modi 
+      p.modifier_for_navigation;
+   output_list 
+      "modifiers_valid" 
+      output_modi 
+      p.modifiers_valid;
+
     close_out fd
   with _ -> prerr_endline "Could not save preferences."
   
@@ -127,6 +138,9 @@ let (current:pref) =
     
     modifier_for_navigation = [`CONTROL; `MOD1];
     modifier_for_templates = [`MOD4];
+    modifier_for_tactics = [`CONTROL; `MOD1];
+    modifiers_valid = [`SHIFT; `CONTROL; `MOD1; `MOD4];
+
     
     cmd_browse = "netscape -remote \"OpenURL(", ")\"";
 
@@ -140,39 +154,45 @@ let load_pref p =
     List.iter 
       (function k,v -> try match k with
 	 | "cmd_coqc" -> p.cmd_coqc <- v
-       | "cmd_make" -> p.cmd_make <-  v
-       | "cmd_coqmakefile" -> p.cmd_coqmakefile <- v
-       | "cmd_coqdoc" -> p.cmd_coqdoc <-  v
-       | "cmd_print" -> p.cmd_print <-  v
-       | "global_auto_revert" -> p.global_auto_revert <- bool_of_string v
-       | "global_auto_revert_delay" -> 
-	   p.global_auto_revert_delay <- int_of_string v
-       | "auto_save" -> p.auto_save <- bool_of_string v
-       | "auto_save_delay" -> p.auto_save_delay <- int_of_string v
-       | "auto_save_prefix" -> 
-	   let x,y = p.auto_save_name in
-	   p.auto_save_name <- (v,y)
-       | "auto_save_suffix" -> 
-	   let x,y = p.auto_save_name in
-	   p.auto_save_name <- (x,v)
-
-       | "cmd_browse_prefix" -> 
-	   let x,y = p.cmd_browse in
-	   p.cmd_browse <- (v,y)
-       | "cmd_browse_suffix" ->
-	   let x,y = p.cmd_browse in
-	   p.cmd_browse <- (x,v)
-       | "doc_url" -> p.doc_url <- v
-       | "library_url" -> p.library_url <- v
-       | "modifier_for_navigation" ->
-	   p.modifier_for_navigation <- 
-	   List.rev_map str_to_mod (Config_lexer.split v)
-       | "modifier_for_templates" ->
-	   p.modifier_for_templates <- 
-	   List.rev_map str_to_mod (Config_lexer.split v)
-       | _ -> prerr_endline ("Warning: unknown option "^k)
-     with _ -> ())
-    l
+	 | "cmd_make" -> p.cmd_make <-  v
+	 | "cmd_coqmakefile" -> p.cmd_coqmakefile <- v
+	 | "cmd_coqdoc" -> p.cmd_coqdoc <-  v
+	 | "cmd_print" -> p.cmd_print <-  v
+	 | "global_auto_revert" -> p.global_auto_revert <- bool_of_string v
+	 | "global_auto_revert_delay" -> 
+	     p.global_auto_revert_delay <- int_of_string v
+	 | "auto_save" -> p.auto_save <- bool_of_string v
+	 | "auto_save_delay" -> p.auto_save_delay <- int_of_string v
+	 | "auto_save_prefix" -> 
+	     let x,y = p.auto_save_name in
+	     p.auto_save_name <- (v,y)
+	 | "auto_save_suffix" -> 
+	     let x,y = p.auto_save_name in
+	     p.auto_save_name <- (x,v)
+	       
+	 | "cmd_browse_prefix" -> 
+	     let x,y = p.cmd_browse in
+	     p.cmd_browse <- (v,y)
+	 | "cmd_browse_suffix" ->
+	     let x,y = p.cmd_browse in
+	     p.cmd_browse <- (x,v)
+	 | "doc_url" -> p.doc_url <- v
+	 | "library_url" -> p.library_url <- v
+	 | "modifier_for_navigation" ->
+	     p.modifier_for_navigation <- 
+	     List.rev_map str_to_mod (Config_lexer.split v)
+	 | "modifier_for_templates" ->
+	     p.modifier_for_templates <- 
+	     List.rev_map str_to_mod (Config_lexer.split v)
+	 | "modifier_for_tactics" ->
+	     p.modifier_for_tactics <- 
+	     List.rev_map str_to_mod (Config_lexer.split v)
+	 | "modifiers_valid" ->
+	     p.modifiers_valid <- 
+	     List.rev_map str_to_mod (Config_lexer.split v)
+	 | _ -> prerr_endline ("Warning: unknown option "^k)
+       with _ -> ())
+      l
   with _ -> prerr_endline "Could not load preferences."
 
 let configure () = 
@@ -199,12 +219,41 @@ let configure () =
       "Global auto revert delay (ms)" 
       (string_of_int current.global_auto_revert_delay)
   in  
+
+  let modifier_for_tactics = 
+    modifiers
+      ~allow:current.modifiers_valid
+      ~f:(fun l -> current.modifier_for_tactics <- l)
+      "Modifiers for Tactics Menu"
+      current.modifier_for_tactics
+  in
+  let modifier_for_templates = 
+    modifiers
+      ~allow:current.modifiers_valid
+      ~f:(fun l -> current.modifier_for_templates <- l)
+      "Modifiers for Templates Menu"
+      current.modifier_for_templates
+  in
+  let modifier_for_navigation = 
+    modifiers
+      ~allow:current.modifiers_valid
+      ~f:(fun l -> current.modifier_for_navigation <- l)
+      "Modifiers for Navigation Menu"
+      current.modifier_for_navigation
+  in
+  let modifiers_valid = 
+    modifiers
+      ~f:(fun l -> current.modifiers_valid <- l)
+      "Allowed modifiers"
+      current.modifiers_valid
+  in
   let cmds =
-      [Section(
-	 "Commands",
-	 [cmd_coqc;cmd_make;cmd_coqmakefile; cmd_coqdoc; cmd_print]);
-       Section ("Files",
-		[global_auto_revert;global_auto_revert_delay])]
+    [Section("Commands",
+	     [cmd_coqc;cmd_make;cmd_coqmakefile; cmd_coqdoc; cmd_print]);
+     Section("Files",
+	     [global_auto_revert;global_auto_revert_delay]);
+     Section("Shortcuts(need restart)",
+	     [modifiers_valid; modifier_for_tactics;modifier_for_templates; modifier_for_navigation])]
   in
   match edit "Customizations" cmds
   with | Return_apply | Return_ok -> save_pref current
diff --git a/ide/undo.ml b/ide/undo.ml
index 1b74926cb1..d172ec605c 100644
--- a/ide/undo.ml
+++ b/ide/undo.ml
@@ -41,7 +41,8 @@ object(self)
 
     end
 
-  method clear_undo = Stack.clear history
+  method clear_undo = Stack.clear history; Stack.clear nredo; Queue.clear redo
+
   method undo = if !undo_lock then begin
     undo_lock := false;
     prerr_endline "UNDO";
diff --git a/ide/utils/configwin.ml b/ide/utils/configwin.ml
index 73ee926e2c..62d3b9d5ab 100644
--- a/ide/utils/configwin.ml
+++ b/ide/utils/configwin.ml
@@ -37,6 +37,7 @@ let combo = Configwin_ihm.combo
 let custom = Configwin_ihm.custom
 let date = Configwin_ihm.date
 let hotkey = Configwin_ihm.hotkey
+let modifiers = Configwin_ihm.modifiers
 let html = Configwin_ihm.html
 
 let edit 
diff --git a/ide/utils/configwin.mli b/ide/utils/configwin.mli
index 1756554177..686b7c8ac0 100644
--- a/ide/utils/configwin.mli
+++ b/ide/utils/configwin.mli
@@ -211,6 +211,11 @@ val hotkey : ?editable: bool -> ?expand: bool -> ?help: string ->
   ?f: ((Gdk.Tags.modifier list * int) -> unit) -> 
     string -> (Gdk.Tags.modifier list * int) -> parameter_kind
 
+val modifiers : ?editable: bool -> ?expand: bool -> ?help: string ->
+  ?allow:(Gdk.Tags.modifier list) ->
+  ?f: (Gdk.Tags.modifier list -> unit) -> 
+    string -> Gdk.Tags.modifier list -> parameter_kind
+
 
 (** [custom box f expand] creates a custom parameter, with
    the given [box], the [f] function is called when the user
diff --git a/ide/utils/configwin_ihm.ml b/ide/utils/configwin_ihm.ml
index f6c4e6daad..04d7c05ede 100644
--- a/ide/utils/configwin_ihm.ml
+++ b/ide/utils/configwin_ihm.ml
@@ -765,6 +765,58 @@ class hotkey_param_box param =
 	()
   end ;;
 
+class modifiers_param_box param =
+  let hbox = GPack.hbox () in
+  let wev = GBin.event_box ~packing: (hbox#pack ~expand: false ~padding: 2) () in
+  let wl = GMisc.label ~text: param.md_label 
+      ~packing: wev#add () 
+  in
+  let we = GEdit.entry
+      ~editable: false
+      ~packing: (hbox#pack ~expand: param.md_expand ~padding: 2)
+      ()
+  in
+  let value = ref param.md_value in
+  let _ = 
+    match param.md_help with
+      None -> ()
+    | Some help ->
+	let tooltips = GData.tooltips () in
+	ignore (hbox#connect#destroy ~callback: tooltips#destroy);
+	tooltips#set_tip wev#coerce ~text: help ~privat: help 
+  in
+  let _ = we#set_text (KeyOption.modifiers_to_string param.md_value) in
+  let mods_we_care = param.md_allow in
+  let capture ev =
+    let modifiers = GdkEvent.Key.state ev in
+    let mods = List.filter
+	(fun m -> (List.mem m mods_we_care))
+	modifiers
+    in
+    value := mods;
+    we#set_text (KeyOption.modifiers_to_string !value);
+    false
+  in
+  let _ = 
+    if param.md_editable then
+      ignore (we#event#connect#key_press capture)
+    else
+      ()
+  in
+
+  object (self)
+    (** This method returns the main box ready to be packed. *)
+    method box = hbox#coerce
+    (** This method applies the new value of the parameter. *)
+    method apply =
+      let new_value = !value in
+      if new_value <> param.md_value then
+	let _ = param.md_f_apply new_value in
+	param.md_value <- new_value
+      else
+	()
+  end ;;
+
 (** This class is used to build a box for a date parameter.*)
 class date_param_box param =
   let v = ref param.date_value in
@@ -891,6 +943,10 @@ class configuration_box conf_struct (notebook : GPack.notebook) =
 		  let box = new hotkey_param_box p in
 		  let _ = main_box#pack ~expand: false ~padding: 2 box#box in
 		  box
+	      |	Modifiers_param p ->
+		  let box = new modifiers_param_box p in
+		  let _ = main_box#pack ~expand: false ~padding: 2 box#box in
+		  box
 	      |	Html_param p ->
 		  let box = new html_param_box p in
 		  let _ = main_box#pack ~expand: p.string_expand ~padding: 2 box#box in
@@ -1093,6 +1149,10 @@ let box param_list buttons =
 	let box = new hotkey_param_box p in
 	let _ = main_box#pack ~expand: false ~padding: 2 box#box in
 	box
+    | Modifiers_param p ->
+	let box = new modifiers_param_box p in
+	let _ = main_box#pack ~expand: false ~padding: 2 box#box in
+	box
     | Html_param p ->
 	let box = new html_param_box p in
 	let _ = main_box#pack ~expand: p.string_expand ~padding: 2 box#box in
@@ -1327,6 +1387,23 @@ let hotkey ?(editable=true) ?(expand=true) ?help ?(f=(fun _ -> ())) label v =
       hk_expand = expand ;
     } 
 
+let modifiers 
+  ?(editable=true) 
+  ?(expand=true) 
+  ?help 
+  ?(allow=[`CONTROL;`SHIFT;`LOCK;`MOD1;`MOD1;`MOD2;`MOD3;`MOD4;`MOD5]) 
+  ?(f=(fun _ -> ())) label v =
+  Modifiers_param
+    {
+      md_label = label ;
+      md_help = help ;
+      md_value = v ;
+      md_editable = editable ;
+      md_f_apply = f ;
+      md_expand = expand ;
+      md_allow = allow ;
+    } 
+
 (** Create a custom param.*)
 let custom ?label box f expand =
   Custom_param
diff --git a/ide/utils/configwin_types.ml b/ide/utils/configwin_types.ml
index 4d8184ebd8..3e09de95f5 100644
--- a/ide/utils/configwin_types.ml
+++ b/ide/utils/configwin_types.ml
@@ -79,6 +79,26 @@ module KeyOption = struct
                      ) ^ s)
         in
         iter m ("-" ^ s)
+
+  let modifiers_to_string m =
+    let rec iter m s =
+      match m with
+          [] -> s
+        | c :: m ->
+            iter m ((
+                      match c with
+			  `CONTROL -> "<ctrl>"
+			| `SHIFT -> "<shft>"
+			| `LOCK -> "<lock>"
+			| `MOD1 -> "<alt>"
+			| `MOD2 -> "<mod2>"
+			| `MOD3 -> "<mod3>"
+			| `MOD4 -> "<mod4>"
+			| `MOD5 -> "<mod5>"
+			| _  -> raise Not_found
+                    ) ^ s)
+    in
+    iter m ""
 	  
   let value_to_key v =
     match v with
@@ -190,6 +210,17 @@ type hotkey_param = {
     hk_expand : bool ; (** expand or not *)
   } 
 
+type modifiers_param = {
+    md_label : string ; (** the label of the parameter *)
+    mutable md_value : Gdk.Tags.modifier list ; 
+             (** The value, as a list of modifiers and a key code *)
+    md_editable : bool ; (** indicates if the value can be changed *)
+    md_f_apply : Gdk.Tags.modifier list -> unit ;
+             (** the function to call to apply the new value of the paramter *)
+    md_help : string option ; (** optional help string *)
+    md_expand : bool ; (** expand or not *)
+    md_allow : Gdk.Tags.modifier list
+  } 
 
 (** This type represents the different kinds of parameters. *)
 type parameter_kind =
@@ -204,6 +235,7 @@ type parameter_kind =
   | Date_param of date_param
   | Font_param of font_param
   | Hotkey_param of hotkey_param
+  | Modifiers_param of modifiers_param
   | Html_param of string_param
 ;;