Merge branch 'v8.5'

13 files changed, 56 insertions, 22 deletions

diff --git a/ide/MacOS/default_accel_map b/ide/MacOS/default_accel_map
index 6f474eb124..47612cdf72 100644
--- a/ide/MacOS/default_accel_map
+++ b/ide/MacOS/default_accel_map
@@ -247,7 +247,6 @@
 ; (gtk_accel_path "<Actions>/Tactics/Tactic constructor" "")
 ; (gtk_accel_path "<Actions>/Tactics/Tactic elim -- with" "")
 ; (gtk_accel_path "<Actions>/Templates/Template Identity Coercion" "")
-; (gtk_accel_path "<Actions>/Queries/Whelp Locate" "")
 (gtk_accel_path "<Actions>/View/Display all low-level contents" "<Shift><Control>l")
 ; (gtk_accel_path "<Actions>/Tactics/Tactic right" "")
 ; (gtk_accel_path "<Actions>/Edit/Find Previous" "<Shift>F3")
diff --git a/ide/coqOps.ml b/ide/coqOps.ml
index 689d4908f7..8ba1c8ecd2 100644
--- a/ide/coqOps.ml
+++ b/ide/coqOps.ml
@@ -218,8 +218,15 @@ object(self)
     let on_click id =
       let find _ _ s = Int.equal s.index id in
       let sentence = Doc.find document find in
-      let mark = sentence.stop in
+      let mark = sentence.start in
       let iter = script#buffer#get_iter_at_mark mark in
+      (** Sentence starts tend to be at the end of a line, so we rather choose
+          the first non-line-ending position. *)
+      let rec sentence_start iter =
+        if iter#ends_line then sentence_start iter#forward_line
+        else iter
+      in
+      let iter = sentence_start iter in
       script#buffer#place_cursor iter;
       ignore (script#scroll_to_iter ~use_align:true ~yalign:0. iter)
     in
diff --git a/ide/coq_commands.ml b/ide/coq_commands.ml
index 995c45c5ae..37e38a5464 100644
--- a/ide/coq_commands.ml
+++ b/ide/coq_commands.ml
@@ -228,8 +228,6 @@ let state_preserving = [
   "Test Printing Synth";
   "Test Printing Wildcard";
 
-  "Whelp Hint";
-  "Whelp Locate";
 ]
 
 
diff --git a/ide/coqide.ml b/ide/coqide.ml
index 5aac8f2a18..4564d620ea 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -852,6 +852,7 @@ let refresh_editor_prefs () =
     Tags.set_processing_color (Tags.color_of_string current.processing_color);
     Tags.set_processed_color (Tags.color_of_string current.processed_color);
     Tags.set_error_color (Tags.color_of_string current.error_color);
+    Tags.set_error_fg_color (Tags.color_of_string current.error_fg_color);
     sn.script#misc#modify_base [`NORMAL, `COLOR clr];
     sn.proof#misc#modify_base [`NORMAL, `COLOR clr];
     sn.messages#misc#modify_base [`NORMAL, `COLOR clr];
@@ -1149,14 +1150,14 @@ let build_ui () =
 
   menu templates_menu [
     item "Templates" ~label:"Te_mplates";
-    template_item ("Lemma new_lemma : .\nProof.\n\nSave.\n", 6,9, "L");
+    template_item ("Lemma new_lemma : .\nProof.\n\nSave.\n", 6,9, "J");
     template_item ("Theorem new_theorem : .\nProof.\n\nSave.\n", 8,11, "T");
     template_item ("Definition ident := .\n", 11,5, "E");
     template_item ("Inductive ident : :=\n  | : .\n", 10,5, "I");
     template_item ("Fixpoint ident (_ : _) {struct _} : _ :=\n.\n", 9,5, "F");
     template_item ("Scheme new_scheme := Induction for _ Sort _\n" ^
                    "with _ := Induction for _ Sort _.\n", 7,10, "S");
-    item "match" ~label:"match ..." ~accel:(prefs.modifier_for_templates^"C")
+    item "match" ~label:"match ..." ~accel:(prefs.modifier_for_templates^"M")
       ~callback:match_callback
   ];
   alpha_items templates_menu "Template" Coq_commands.commands;
@@ -1164,13 +1165,12 @@ let build_ui () =
   let qitem s accel = item s ~label:("_"^s) ?accel ~callback:(Query.query s) in
   menu queries_menu [
     item "Queries" ~label:"_Queries";
-    qitem "Search" (Some "F2");
-    qitem "Check" (Some "F3");
-    qitem "Print" (Some "F4");
-    qitem "About" (Some "F5");
-    qitem "Locate" None;
-    qitem "Print Assumptions" None;
-    qitem "Whelp Locate" None;
+    qitem "Search" (Some "<Ctrl><Shift>K");
+    qitem "Check" (Some "<Ctrl><Shift>C");
+    qitem "Print" (Some "<Ctrl><Shift>P");
+    qitem "About" (Some "<Ctrl><Shift>A");
+    qitem "Locate" (Some "<Ctrl><Shift>L");
+    qitem "Print Assumptions" (Some "<Ctrl><Shift>N");
   ];
 
   menu tools_menu [
@@ -1333,6 +1333,11 @@ let build_ui () =
       (Gdk.Bitmap.create_from_data ~width:2 ~height:2 "\x01\x02"));
   Tags.Script.incomplete#set_property
     (`BACKGROUND_GDK (Tags.get_processed_color ())); 
+  Tags.Script.read_only#set_property
+    (`BACKGROUND_STIPPLE
+      (Gdk.Bitmap.create_from_data ~width:2 ~height:2 "\x01\x02"));
+  Tags.Script.read_only#set_property
+    (`BACKGROUND_GDK (Tags.get_processed_color ())); 
 
   (* Showtime ! *)
   w#show ()
diff --git a/ide/coqide_ui.ml b/ide/coqide_ui.ml
index af71b1e78c..edfe28b261 100644
--- a/ide/coqide_ui.ml
+++ b/ide/coqide_ui.ml
@@ -119,7 +119,6 @@ let init () =
     <menuitem action='About' />
     <menuitem action='Locate' />
     <menuitem action='Print Assumptions' />
-    <menuitem action='Whelp Locate' />
   </menu>
   <menu name='Tools' action='Tools'>
     <menuitem action='Comment' />
diff --git a/ide/gtk_parsing.ml b/ide/gtk_parsing.ml
index abbd7e6d59..79ccf61a43 100644
--- a/ide/gtk_parsing.ml
+++ b/ide/gtk_parsing.ml
@@ -166,3 +166,16 @@ let find_nearest_backward (cursor:GText.iter) targets =
       | None -> raise Not_found
       | Some nearest -> nearest
 
+(** On double-click on a view, select the whole word. This is a workaround for
+    a deficient word handling in TextView. *)
+let fix_double_click self =
+  let callback ev = match GdkEvent.get_type ev with
+  | `TWO_BUTTON_PRESS ->
+    let iter = self#buffer#get_iter `INSERT in
+    let start, stop = get_word_around iter in
+    let () = self#buffer#move_mark `INSERT ~where:start in
+    let () = self#buffer#move_mark `SEL_BOUND ~where:stop in
+    true
+  | _ -> false
+  in
+  ignore (self#event#connect#button_press ~callback)
diff --git a/ide/ideutils.ml b/ide/ideutils.ml
index 84ef8f40db..473b8dc82e 100644
--- a/ide/ideutils.ml
+++ b/ide/ideutils.ml
@@ -132,8 +132,6 @@ let mktimer () =
              with Glib.GError _ -> ());
              timer := None) }
 
-let last_dir = ref ""
-
 let filter_all_files () = GFile.filter
   ~name:"All"
   ~patterns:["*"] ()
@@ -142,6 +140,10 @@ let filter_coq_files () =  GFile.filter
   ~name:"Coq source code"
   ~patterns:[ "*.v"] ()
 
+let current_dir () = match current.project_path with
+| None -> ""
+| Some dir -> dir
+
 let select_file_for_open ~title () =
   let file = ref None in
   let file_chooser =
@@ -152,14 +154,14 @@ let select_file_for_open ~title () =
   file_chooser#add_filter (filter_coq_files ());
   file_chooser#add_filter (filter_all_files ());
   file_chooser#set_default_response `OPEN;
-  ignore (file_chooser#set_current_folder !last_dir);
+  ignore (file_chooser#set_current_folder (current_dir ()));
   begin match file_chooser#run () with
     | `OPEN ->
       begin
 	file := file_chooser#filename;
 	match !file with
 	  | None -> ()
-	  | Some s -> last_dir := Filename.dirname s;
+	  | Some s -> current.project_path <- file_chooser#current_folder
       end
     | `DELETE_EVENT | `CANCEL -> ()
   end ;
@@ -178,7 +180,7 @@ let select_file_for_save ~title ?filename () =
   file_chooser#set_do_overwrite_confirmation true;
   file_chooser#set_default_response `SAVE;
   let dir,filename = match filename with
-    |None -> !last_dir, ""
+    |None -> current_dir (), ""
     |Some f -> Filename.dirname f, Filename.basename f
   in
   ignore (file_chooser#set_current_folder dir);
@@ -189,7 +191,7 @@ let select_file_for_save ~title ?filename () =
         file := file_chooser#filename;
         match !file with
             None -> ()
-          | Some s -> last_dir := Filename.dirname s;
+          | Some s -> current.project_path <- file_chooser#current_folder
       end
     | `DELETE_EVENT | `CANCEL -> ()
   end ;
diff --git a/ide/preferences.ml b/ide/preferences.ml
index 9a4fde2f6e..c59642d3a7 100644
--- a/ide/preferences.ml
+++ b/ide/preferences.ml
@@ -105,6 +105,7 @@ type pref =
 
       mutable read_project : project_behavior;
       mutable project_file_name : string;
+      mutable project_path : string option;
 
       mutable encoding : inputenc;
 
@@ -180,8 +181,9 @@ let current = {
     source_language = "coq";
     source_style = "coq_style";
 
-    read_project = Ignore_args;
+    read_project = Append_args;
     project_file_name = "_CoqProject";
+    project_path = None;
 
     encoding = if Sys.os_type = "Win32" then Eutf8 else Elocale;
 
@@ -265,6 +267,7 @@ let save_pref () =
 
     add "project_options" [string_of_project_behavior p.read_project] ++
     add "project_file_name" [p.project_file_name] ++
+    add "project_path" (match p.project_path with None -> [] | Some s -> [s]) ++
 
     add "encoding" [string_of_inputenc p.encoding] ++
 
@@ -342,6 +345,7 @@ let load_pref () =
     set_hd "project_options"
       (fun v -> np.read_project <- (project_behavior_of_string v));
     set_hd "project_file_name" (fun v -> np.project_file_name <- v);
+    set_option "project_path" (fun v -> np.project_path <- v);
     set "automatic_tactics"
       (fun v -> np.automatic_tactics <- v);
     set_hd "cmd_print" (fun v -> np.cmd_print <- v);
diff --git a/ide/preferences.mli b/ide/preferences.mli
index ab12e4c7ba..1e4f152c23 100644
--- a/ide/preferences.mli
+++ b/ide/preferences.mli
@@ -32,6 +32,7 @@ type pref =
 
       mutable read_project : project_behavior;
       mutable project_file_name : string;
+      mutable project_path : string option;
 
       mutable encoding : inputenc;
 
diff --git a/ide/tags.ml b/ide/tags.ml
index 079cf94853..d4460b0770 100644
--- a/ide/tags.ml
+++ b/ide/tags.ml
@@ -52,7 +52,9 @@ struct
     t
   let all = edit_zone :: all
   
-  let read_only = make_tag table ~name:"read_only" [`EDITABLE false ]
+  let read_only = make_tag table ~name:"read_only" [`EDITABLE false;
+          `BACKGROUND !processing_color;
+          `BACKGROUND_STIPPLE_SET true ]
 
 end
 module Proof =
@@ -94,6 +96,7 @@ let set_processing_color clr =
   let s = string_of_color clr in
   processing_color := s;
   Script.incomplete#set_property (`BACKGROUND s);
+  Script.read_only#set_property (`BACKGROUND s);
   Script.to_process#set_property (`BACKGROUND s)
 
 let get_error_color () = color_of_string !error_color
diff --git a/ide/wg_MessageView.ml b/ide/wg_MessageView.ml
index 09f1d44535..b32674084d 100644
--- a/ide/wg_MessageView.ml
+++ b/ide/wg_MessageView.ml
@@ -48,6 +48,7 @@ let message_view () : message_view =
     ~source_buffer:buffer ~packing:scroll#add
     ~editable:false ~cursor_visible:false ~wrap_mode:`WORD ()
   in
+  let () = Gtk_parsing.fix_double_click view in
   let default_clipboard = GData.clipboard Gdk.Atom.primary in
   let _ = buffer#add_selection_clipboard default_clipboard in
   let () = view#set_left_margin 2 in
diff --git a/ide/wg_ProofView.ml b/ide/wg_ProofView.ml
index a33f2c591c..b12d29d6c9 100644
--- a/ide/wg_ProofView.ml
+++ b/ide/wg_ProofView.ml
@@ -181,6 +181,7 @@ let proof_view () =
   let view = GSourceView2.source_view
     ~source_buffer:buffer ~editable:false ~wrap_mode:`WORD ()
   in
+  let () = Gtk_parsing.fix_double_click view in
   let default_clipboard = GData.clipboard Gdk.Atom.primary in
   let _ = buffer#add_selection_clipboard default_clipboard in
   object
diff --git a/ide/wg_ScriptView.ml b/ide/wg_ScriptView.ml
index 5d21efd956..8298d9954f 100644
--- a/ide/wg_ScriptView.ml
+++ b/ide/wg_ScriptView.ml
@@ -418,6 +418,7 @@ object (self)
       self#buffer#end_user_action ()
 
   initializer
+    let () = Gtk_parsing.fix_double_click self in
     let supersed cb _ =
       let _ = cb () in
       GtkSignal.stop_emit()