Imported Upstream version 8.5~beta2+dfsgupstream/8.5_beta2+dfsg

26 files changed, 357 insertions, 154 deletions

diff --git a/ide/MacOS/Info.plist.template b/ide/MacOS/Info.plist.template
index fd80c839..e224e812 100644
--- a/ide/MacOS/Info.plist.template
+++ b/ide/MacOS/Info.plist.template
@@ -66,7 +66,7 @@
 	<key>CFBundleGetInfoString</key>
 	<string>Coq_vVERSION</string>
 	<key>NSHumanReadableCopyright</key>
-	<string>Copyright 1999-2014, The Coq Development Team INRIA - CNRS - LIX - LRI - PPS</string>
+	<string>Copyright 1999-2015, The Coq Development Team INRIA - CNRS - LIX - LRI - PPS</string>
 	<key>CFBundleHelpBookFolder</key>
 	<string>share/doc/coq/html/</string>
 	<key>CFAppleHelpAnchor</key>
diff --git a/ide/MacOS/default_accel_map b/ide/MacOS/default_accel_map
index 6f474eb1..47612cdf 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/coq.lang b/ide/coq.lang
index 608a4aea..65150d6a 100644
--- a/ide/coq.lang
+++ b/ide/coq.lang
@@ -22,19 +22,19 @@
   </styles>
   
   <definitions>
-    <define-regex id="space">\s</define-regex>
+    <define-regex id="space">\s+</define-regex>
     <define-regex id="first_ident_char">[_\p{L}]</define-regex>
     <define-regex id="ident_char">[_\p{L}'\pN]</define-regex>
     <define-regex id="ident">\%{first_ident_char}\%{ident_char}*</define-regex>
     <define-regex id="qualit">(\%{ident}\.)*\%{ident}</define-regex>
     <define-regex id="undotted_sep">[-+*{}]</define-regex>
     <define-regex id="dot_sep">\.(\s|\z)</define-regex>
-    <define-regex id="single_decl">(Definition)|(Let)|(Example)|(SubClass)|(Fixpoint)|(CoFixpoint)|(Scheme)|(Function)|(Hypothesis)|(Axiom)|(Variable)|(Parameter)|(Conjecture)|(Inductive)|(CoInductive)|(Record)|(Structure)|(Ltac)|(Instance)|(Context)|(Class)|(Module(\%{space}+Type)?)|(Existing\%{space}+Instance)|(Canonical\%{space}+Structure)</define-regex>
-    <define-regex id="mult_decl">(Hypotheses)|(Axioms)|(Variables)|(Parameters)|(Implicit\%{space}+Type(s)?)</define-regex>
-    <define-regex id="locality">(((Local)|(Global))\%{space}+)?</define-regex>
-    <define-regex id="begin_proof">(Theorem)|(Lemma)|(Fact)|(Remark)|(Corollary)|(Proposition)|(Property)</define-regex>
-    <define-regex id="end_proof">(Qed)|(Defined)|(Admitted)|(Abort)</define-regex>
-    <define-regex id="decl_head">((?'gal'\%{locality}(Program\%{space}+)?(\%{single_decl}|\%{begin_proof}))\%{space}+(?'id'\%{ident}))|((?'gal4list'\%{mult_decl})(?'id_list'(\%{space}+\%{ident})*))|(?'gal2'Goal)</define-regex>
+    <define-regex id="single_decl">Definition|Let|Example|SubClass|(Co)?Fixpoint|Function|Conjecture|(Co)?Inductive|Record|Structure|Ltac|Instance|Class|Existing\%{space}Instance|Canonical\%{space}Structure|Coercion</define-regex>
+    <define-regex id="mult_decl">Hypothes[ie]s|Axiom(s)?|Variable(s)?|Parameter(s)?|Context|Implicit\%{space}Type(s)?</define-regex>
+    <define-regex id="locality">((Local|Global)\%{space})?</define-regex>
+    <define-regex id="begin_proof">Theorem|Lemma|Fact|Remark|Corollary|Proposition|Property</define-regex>
+    <define-regex id="end_proof">Qed|Defined|Admitted|Abort|Save</define-regex>
+    <define-regex id="decl_head">((?'gal'\%{locality}(Program\%{space})?(\%{single_decl}|\%{begin_proof}))\%{space}(?'id'\%{ident}))|((?'gal4list'\%{mult_decl})(?'id_list'(\%{space}\%{ident})*))|(?'gal2'Goal)</define-regex>
 
     <context id="escape-seq" style-ref="escape">
       <match>""</match>
@@ -97,7 +97,6 @@
 	      <keyword>then</keyword>
 	      <keyword>else</keyword>
 	      <keyword>return</keyword>
-	      <keyword>using</keyword>
 	    </context>
 	    <context id="constr-sort" style-ref="constr-sort">
 	      <keyword>Prop</keyword>
@@ -113,7 +112,7 @@
 	  </include>
 	</context>
 	<context id="proof">
-	  <start>Proof(\%{dot_sep}|\%{space}+(using)|\%{space}+(with))</start>
+	  <start>Proof(\%{dot_sep}|\%{space}using|\%{space}with)</start>
 	  <end>\%{end_proof}\%{dot_sep}</end>
 	  <include>
 	    <context sub-pattern="0" where="start" style-ref="vernac-keyword"/>
@@ -157,17 +156,18 @@
 	  <keyword>Eval</keyword>
 	  <keyword>Load</keyword>
 	  <keyword>Undo</keyword>
+	  <keyword>(Print|Reset)\%{space}+Extraction\%{space}+(Inline|Blacklist)</keyword>
 	  <keyword>Print</keyword>
-	  <keyword>Save</keyword>
 	  <keyword>Comments</keyword>
-	  <keyword>Solve\%{space}+Obligation</keyword>
-	  <keyword>((Uns)|(S))et(\%{space}+\%{ident})+</keyword>
-	  <keyword>(\%{locality}|((Reserved)|(Tactic))\%{space}+)?Notation</keyword>
+	  <keyword>Solve\%{space}Obligation</keyword>
+	  <keyword>(Uns|S)et(\%{space}\%{ident})+</keyword>
+	  <keyword>(\%{locality}|(Reserved|Tactic)\%{space})?Notation</keyword>
 	  <keyword>\%{locality}Infix</keyword>
-	  <keyword>(Print)|(Reset)\%{space}+Extraction\%{space}+(Inline)|(Blacklist)</keyword>
+	  <keyword>Declare\%{space}ML\%{space}Module</keyword>
+	  <keyword>Extraction\%{space}Language\%{space}(Ocaml|Haskell|Scheme|JSON)</keyword>
 	</context>
 	<context id="hint-command" style-ref="vernac-keyword">
-	  <prefix>\%{locality}Hint\%{space}+</prefix>
+	  <prefix>\%{locality}Hint\%{space}</prefix>
 	  <keyword>Resolve</keyword>
 	  <keyword>Immediate</keyword>
 	  <keyword>Constructors</keyword>
@@ -178,35 +178,40 @@
 	  <keyword>Rewrite</keyword>
 	</context>
 	<context id="scope-command" style-ref="vernac-keyword">
-	  <suffix>\%{space}+Scope</suffix>
+	  <suffix>\%{space}Scope</suffix>
 	  <keyword>\%{locality}Open</keyword>
 	  <keyword>\%{locality}Close</keyword>
 	  <keyword>Bind</keyword>
 	  <keyword>Delimit</keyword>
 	</context>
 	<context id="command-for-qualit">
-	  <suffix>\%{space}+(?'qua'\%{qualit})</suffix>
+	  <suffix>\%{space}(?'qua'\%{qualit})</suffix>
 	  <keyword>Chapter</keyword>
-	  <keyword>Combined\%{space}+Scheme</keyword>
+	  <keyword>Combined\%{space}Scheme</keyword>
+	  <keyword>Scheme\%{space}(Induction|Minimality|Elimination|Case|Equality)\%{space}for</keyword>
 	  <keyword>End</keyword>
 	  <keyword>Section</keyword>
+	  <keyword>Module(\%{space}Type)?</keyword>
+	  <keyword>Declare\%{space}Module(\%{space}(Import|Export))?</keyword>
+	  <keyword>About</keyword>
 	  <keyword>Arguments</keyword>
-	  <keyword>Implicit\%{space}+Arguments</keyword>
-	  <keyword>Import</keyword>
+	  <keyword>Implicit\%{space}Arguments</keyword>
 	  <keyword>Include</keyword>
-	  <keyword>Export</keyword>
-	  <keyword>Require(\%{space}+((Import)|(Export)))?</keyword>
-	  <keyword>(Recursive\%{space}+)?Extraction(\%{space}+(Language\%{space}+(Ocaml)|(Haskell)|(Scheme)|(Toplevel))|(Library)|((No)?Inline)|(Blacklist))?</keyword>
-	  <keyword>Extract\%{space}+(Inlined\%{space}+)?(Constant)|(Inductive)</keyword>
+	  <keyword>Extract\%{space}((Inlined\%{space})?Constant|Inductive)</keyword>
 	  <include>
 	    <context sub-pattern="1" style-ref="vernac-keyword"/>
 	    <context sub-pattern="qua" style-ref="identifier"/>
 	  </include>
 	</context>
-	<context id="command-for-qualit-list" style-ref="vernac-keyword">
-	  <suffix>(?'qua_list'(\%{space}+\%{qualit})+)</suffix>
-	  <keyword>Typeclasses (Transparent)|(Opaque)</keyword>
+	<context id="command-for-qualit-list">
+	  <suffix>(?'qua_list'(\%{space}\%{qualit})+)</suffix>
+	  <keyword>Typeclasses (Transparent|Opaque)</keyword>
+	  <keyword>Require(\%{space}(Import|Export))?</keyword>
+	  <keyword>Import</keyword>
+	  <keyword>Export</keyword>
+	  <keyword>((Recursive|Separate)\%{space})?Extraction(\%{space}(Library|(No)?Inline|Blacklist))?</keyword>
 	  <include>
+	    <context sub-pattern="1" style-ref="vernac-keyword"/>
 	    <context sub-pattern="qua_list" style-ref="identifier"/>
 	  </include>
 	</context>
diff --git a/ide/coqOps.ml b/ide/coqOps.ml
index 52e18456..af728471 100644
--- a/ide/coqOps.ml
+++ b/ide/coqOps.ml
@@ -215,8 +215,24 @@ object(self)
       document_length <- pred document_length;
       segment#set_length document_length;
     in
+    let on_click id =
+      let find _ _ s = Int.equal s.index id in
+      let sentence = Doc.find document find 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
     let _ = (Doc.connect document)#pushed on_push in
     let _ = (Doc.connect document)#popped on_pop in
+    let _ = segment#connect#clicked on_click in
     ()
 
   method private tooltip_callback ~x ~y ~kbd tooltip =
@@ -260,21 +276,11 @@ object(self)
     Doc.focus document ~cond_top:(at start) ~cond_bot:(at stop);
     self#print_stack;
     let qed_s = Doc.tip_data document in
-    buffer#apply_tag Tags.Script.read_only
-      ~start:((buffer#get_iter_at_mark qed_s.start)#forward_find_char
-        (fun c -> not(Glib.Unichar.isspace c)))
-      ~stop:(buffer#get_iter_at_mark qed_s.stop);
     buffer#move_mark ~where:(buffer#get_iter_at_mark qed_s.stop)
       (`NAME "stop_of_input")
 
   method private exit_focus =
     Minilib.log "Unfocusing";
-    begin try
-      let { start; stop } = Doc.tip_data document in
-      buffer#remove_tag Tags.Script.read_only
-        ~start:(buffer#get_iter_at_mark start)
-        ~stop:(buffer#get_iter_at_mark stop)
-    with Doc.Empty -> () end;
     Doc.unfocus document;
     self#print_stack;
     begin try
@@ -347,7 +353,7 @@ object(self)
        else if has_flag sentence `ERROR then [error_bg]
        else if has_flag sentence `INCOMPLETE then [incomplete]
        else [processed]) @
-      (if [ `UNSAFE ] = sentence.flags then [unjustified] else [])
+      (if has_flag sentence `UNSAFE then [unjustified] else [])
     in
     List.iter (fun t -> buffer#remove_tag t ~start ~stop) all_tags;
     List.iter (fun t -> buffer#apply_tag t ~start ~stop) tags
@@ -499,7 +505,7 @@ object(self)
       | Some (start, stop) ->
         if until n start stop then begin
           ()
-        end else if start#has_tag Tags.Script.processed then begin
+        end else if stop#backward_char#has_tag Tags.Script.processed then begin
           Queue.push (`Skip (start, stop)) queue;
           loop n stop
         end else begin
@@ -547,12 +553,15 @@ object(self)
       script#recenter_insert;
       match topstack with
       | [] -> self#show_goals_aux ?move_insert ()
-      | (_,s) :: _ -> self#backtrack_to_iter (buffer#get_iter_at_mark s.start) in
+      | (_,s)::_ -> self#backtrack_to_iter (buffer#get_iter_at_mark s.start) in
     let process_queue queue =
       let rec loop tip topstack =
         if Queue.is_empty queue then conclude topstack else
         match Queue.pop queue, topstack with
-        | `Skip(start,stop), [] -> assert false
+        | `Skip(start,stop), [] ->
+            logger Pp.Error "You muse close the proof with Qed or Admitted";
+            self#discard_command_queue queue;
+            conclude [] 
         | `Skip(start,stop), (_,s) :: topstack ->
             assert(start#equal (buffer#get_iter_at_mark s.start));
             assert(stop#equal (buffer#get_iter_at_mark s.stop));
@@ -646,10 +655,13 @@ object(self)
       buffer#remove_tag Tags.Script.unjustified ~start ~stop;
       buffer#remove_tag Tags.Script.tooltip ~start ~stop;
       buffer#remove_tag Tags.Script.to_process ~start ~stop;
+      buffer#remove_tag Tags.Script.error ~start ~stop;
+      buffer#remove_tag Tags.Script.error_bg ~start ~stop;
       buffer#move_mark ~where:start (`NAME "start_of_input")
     end;
     List.iter (fun { start } -> buffer#delete_mark start) seg;
-    List.iter (fun { stop } -> buffer#delete_mark stop) seg
+    List.iter (fun { stop } -> buffer#delete_mark stop) seg;
+    self#print_stack
 
   (** Wrapper around the raw undo command *)
   method private backtrack_to_id ?(move_insert=true) (to_id, unfocus_needed) =
diff --git a/ide/coq_commands.ml b/ide/coq_commands.ml
index 995c45c5..37e38a54 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 fa64defa..0f4cb7b0 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -84,14 +84,15 @@ let pr_exit_status = function
   | _ -> " failed"
 
 let make_coqtop_args = function
-  |None -> !sup_args
+  |None -> "", !sup_args
   |Some the_file ->
     let get_args f = Project_file.args_from_project f
       !custom_project_files prefs.project_file_name
     in
     match prefs.read_project with
-      |Ignore_args -> !sup_args
-      |Append_args -> get_args the_file @ !sup_args
+      |Ignore_args -> "", !sup_args
+      |Append_args ->
+         let fname, args = get_args the_file in fname, args @ !sup_args
       |Subst_args -> get_args the_file
 
 (** Setting drag & drop on widgets *)
@@ -120,7 +121,10 @@ let set_drag (w : GObj.drag_ops) =
 (** Session management *)
 
 let create_session f =
-  let ans = Session.create f (make_coqtop_args f) in
+  let project_file, args = make_coqtop_args f in
+  if project_file <> "" then
+    flash_info (Printf.sprintf "Reading options from %s" project_file);
+  let ans = Session.create f args in
   let _ = set_drag ans.script#drag in
   ans
 
@@ -249,11 +253,14 @@ let newfile _ =
   !refresh_editor_hook ();
   notebook#goto_page index
 
-let load _ =
-  match select_file_for_open ~title:"Load file" () with
+let load sn =
+  let filename = sn.fileops#filename in
+  match select_file_for_open ~title:"Load file" ?filename () with
     | None -> ()
     | Some f -> FileAux.load_file f
 
+let load = cb_on_current_term load
+
 let save _ = on_current_term (FileAux.check_save ~saveas:false)
 
 let saveas sn =
@@ -530,7 +537,7 @@ let update_status sn =
       | None -> ""
       | Some n -> ", proving " ^ n
     in
-    display ("Ready"^ if current.nanoPG then ", [μPG]" else "" ^ path ^ name);
+    display ("Ready"^ (if current.nanoPG then ", [μPG]" else "") ^ path ^ name);
     Coq.return ()
   in
   Coq.bind (Coq.status ~logger:sn.messages#push false) next
@@ -588,13 +595,24 @@ let get_current_word term =
   | Some p -> p
   | None ->
   (** Then look at the current selected word *)
-  if term.script#buffer#has_selection then
-    let (start, stop) = term.script#buffer#selection_bounds in
+  let buf1 = term.script#buffer in
+  let buf2 = term.proof#buffer in
+  let buf3 = term.messages#buffer in
+  if buf1#has_selection then
+    let (start, stop) = buf1#selection_bounds in
+    buf1#get_text ~slice:true ~start ~stop ()
+  else if buf2#has_selection then
+    let (start, stop) = buf2#selection_bounds in
+    buf2#get_text ~slice:true ~start ~stop ()
+  else if buf3#has_selection then
+    let (start, stop) = buf3#selection_bounds in
+    buf3#get_text ~slice:true ~start ~stop ()
+  (** Otherwise try to find the word around the cursor *)
+  else
+    let it = term.script#buffer#get_iter_at_mark `INSERT in
+    let start = find_word_start it in
+    let stop = find_word_end start in
     term.script#buffer#get_text ~slice:true ~start ~stop ()
-  (** Otherwise try to recover the clipboard *)
-  else match Ideutils.cb#text with
-  | Some t -> t
-  | None -> ""
 
 let print_branch c l =
   Format.fprintf c " | @[<hov 1>%a@]=> _@\n"
@@ -838,10 +856,16 @@ let refresh_editor_prefs () =
     sn.command#refresh_font ();
 
     (* Colors *)
+    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];
-    sn.command#refresh_color ()
+    sn.messages#refresh_color ();
+    sn.command#refresh_color ();
+    sn.errpage#refresh_color ();
+    sn.jobpage#refresh_color ();
 
   in
   List.iter iter_session notebook#pages
@@ -1135,14 +1159,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;
@@ -1150,13 +1174,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 [
@@ -1314,8 +1337,6 @@ let build_ui () =
   refresh_tabs_hook := refresh_notebook_pos;
 
   (* Color configuration *)
-  Tags.set_processing_color (Tags.color_of_string prefs.processing_color);
-  Tags.set_processed_color (Tags.color_of_string prefs.processed_color);
   Tags.Script.incomplete#set_property
     (`BACKGROUND_STIPPLE
       (Gdk.Bitmap.create_from_data ~width:2 ~height:2 "\x01\x02"));
diff --git a/ide/coqide_ui.ml b/ide/coqide_ui.ml
index af71b1e7..edfe28b2 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 abbd7e6d..79ccf61a 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/ide_slave.ml b/ide/ide_slave.ml
index ac38f1ea..dc52ea9a 100644
--- a/ide/ide_slave.ml
+++ b/ide/ide_slave.ml
@@ -123,7 +123,7 @@ let annotate phrase =
     let pa = Pcoq.Gram.parsable (Stream.of_string phrase) in
     Vernac.parse_sentence (pa,None)
   in
-  let (_, _, xml) =
+  let (_, xml) =
     Richprinter.richpp_vernac ast
   in
   xml
@@ -327,14 +327,14 @@ let handle_exn (e, info) =
   let loc_of e = match Loc.get_loc e with
     | Some loc when not (Loc.is_ghost loc) -> Some (Loc.unloc loc)
     | _ -> None in
-  let mk_msg e = read_stdout ()^"\n"^string_of_ppcmds (Errors.print e) in
+  let mk_msg () = read_stdout ()^"\n"^string_of_ppcmds (Errors.print ~info e) in
   match e with
   | Errors.Drop -> dummy, None, "Drop is not allowed by coqide!"
   | Errors.Quit -> dummy, None, "Quit is not allowed by coqide!"
   | e ->
       match Stateid.get info with
-      | Some (valid, _) -> valid, loc_of info, mk_msg e
-      | None -> dummy, loc_of info, mk_msg e
+      | Some (valid, _) -> valid, loc_of info, mk_msg ()
+      | None -> dummy, loc_of info, mk_msg ()
 
 let init =
   let initialized = ref false in
diff --git a/ide/ideutils.ml b/ide/ideutils.ml
index d2305b58..67e4bdb0 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,8 +140,11 @@ let filter_coq_files () =  GFile.filter
   ~name:"Coq source code"
   ~patterns:[ "*.v"] ()
 
-let select_file_for_open ~title () =
-  let file = ref None in
+let current_dir () = match current.project_path with
+| None -> ""
+| Some dir -> dir
+
+let select_file_for_open ~title ?filename () =
   let file_chooser =
     GWindow.file_chooser_dialog ~action:`OPEN ~modal:true ~title ()
   in
@@ -152,19 +153,22 @@ 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);
-  begin match file_chooser#run () with
+  let dir = match filename with
+    | None -> current_dir ()
+    | Some f -> Filename.dirname f in
+  ignore (file_chooser#set_current_folder dir);
+  let file =
+    match file_chooser#run () with
     | `OPEN ->
       begin
-	file := file_chooser#filename;
-	match !file with
-	  | None -> ()
-	  | Some s -> last_dir := Filename.dirname s;
+	match file_chooser#filename with
+	  | None -> None
+	  | Some _ as f ->
+            current.project_path <- file_chooser#current_folder; f
       end
-    | `DELETE_EVENT | `CANCEL -> ()
-  end ;
+    | `DELETE_EVENT | `CANCEL -> None in
   file_chooser#destroy ();
-  !file
+  file
 
 let select_file_for_save ~title ?filename () =
   let file = ref None in
@@ -175,13 +179,10 @@ let select_file_for_save ~title ?filename () =
   file_chooser#add_select_button_stock `SAVE `SAVE ;
   file_chooser#add_filter (filter_coq_files ());
   file_chooser#add_filter (filter_all_files ());
-  (* this line will be used when a lablgtk >= 2.10.0 is the default
-     on most distributions:
-     file_chooser#set_do_overwrite_confirmation true;
-  *)
+  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);
@@ -192,7 +193,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 ;
@@ -246,7 +247,14 @@ let coqtop_path () =
 	    let i = Str.search_backward (Str.regexp_string "coqide") prog pos
             in
 	    String.blit "coqtop" 0 prog i 6;
-	    if Sys.file_exists prog then prog else "coqtop"
+	    if Sys.file_exists prog then prog
+	    else
+	      let in_macos_bundle =
+		Filename.concat
+		  (Filename.dirname prog)
+		  (Filename.concat "../Resources/bin" (Filename.basename prog))
+	      in if Sys.file_exists in_macos_bundle then in_macos_bundle
+		 else "coqtop"
 	  with Not_found -> "coqtop"
   in file
 
@@ -279,7 +287,7 @@ let default_logger level message =
 
 (** {6 File operations} *)
 
-(** A customized [stat] function. Exceptions are catched. *)
+(** A customized [stat] function. Exceptions are caught. *)
 
 type stats = MTime of float | NoSuchFile | OtherError
 
diff --git a/ide/ideutils.mli b/ide/ideutils.mli
index 8269582d..1fb30e4d 100644
--- a/ide/ideutils.mli
+++ b/ide/ideutils.mli
@@ -29,7 +29,7 @@ val find_tag_limits : GText.tag -> GText.iter -> GText.iter * GText.iter
 val find_tag_start : GText.tag -> GText.iter -> GText.iter
 val find_tag_stop : GText.tag -> GText.iter -> GText.iter
 
-val select_file_for_open : title:string -> unit -> string option
+val select_file_for_open : title:string -> ?filename:string -> unit -> string option
 val select_file_for_save :
   title:string -> ?filename:string -> unit -> string option
 val try_convert : string -> string
@@ -71,7 +71,7 @@ val default_logger : Pp.message_level -> string -> unit
 
 (** {6 I/O operations} *)
 
-(** A customized [stat] function. Exceptions are catched. *)
+(** A customized [stat] function. Exceptions are caught. *)
 
 type stats = MTime of float | NoSuchFile | OtherError
 val stat : string -> stats
diff --git a/ide/preferences.ml b/ide/preferences.ml
index c8506132..c59642d3 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;
 
@@ -144,6 +145,7 @@ type pref =
       mutable processing_color : string;
       mutable processed_color : string;
       mutable error_color : string;
+      mutable error_fg_color : string;
 
       mutable dynamic_word_wrap : bool;
       mutable show_line_number : bool;
@@ -179,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;
 
@@ -220,10 +223,11 @@ let current = {
     vertical_tabs = false;
     opposite_tabs = false;
 
-    background_color = "cornsilk";
-    processed_color = "light green";
-    processing_color = "light blue";
-    error_color = "#FFCCCC";
+    background_color = Tags.default_color;
+    processed_color = Tags.default_processed_color;
+    processing_color = Tags.default_processing_color;
+    error_color = Tags.default_error_color;
+    error_fg_color = Tags.default_error_fg_color;
 
     dynamic_word_wrap = false;
     show_line_number = false;
@@ -263,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] ++
 
@@ -296,6 +301,7 @@ let save_pref () =
     add "processing_color" [p.processing_color] ++
     add "processed_color" [p.processed_color] ++
     add "error_color" [p.error_color] ++
+    add "error_fg_color" [p.error_fg_color] ++
     add "dynamic_word_wrap" [string_of_bool p.dynamic_word_wrap] ++
     add "show_line_number" [string_of_bool p.show_line_number] ++
     add "auto_indent" [string_of_bool p.auto_indent] ++
@@ -339,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);
@@ -382,6 +389,7 @@ let load_pref () =
     set_hd "processing_color" (fun v -> np.processing_color <- v);
     set_hd "processed_color" (fun v -> np.processed_color <- v);
     set_hd "error_color" (fun v -> np.error_color <- v);
+    set_hd "error_fg_color" (fun v -> np.error_fg_color <- v);
     set_bool "dynamic_word_wrap" (fun v -> np.dynamic_word_wrap <- v);
     set_bool "show_line_number" (fun v -> np.show_line_number <- v);
     set_bool "auto_indent" (fun v -> np.auto_indent <- v);
@@ -466,10 +474,15 @@ let configure ?(apply=(fun () -> ())) () =
       ~text:"Background color of errors"
       ~packing:(table#attach ~expand:`X ~left:0 ~top:3) ()
     in
+    let error_fg_label = GMisc.label
+      ~text:"Foreground color of errors"
+      ~packing:(table#attach ~expand:`X ~left:0 ~top:4) ()
+    in
     let () = background_label#set_xalign 0. in
     let () = processed_label#set_xalign 0. in
     let () = processing_label#set_xalign 0. in
     let () = error_label#set_xalign 0. in
+    let () = error_fg_label#set_xalign 0. in
     let background_button = GButton.color_button
       ~color:(Tags.color_of_string (current.background_color))
       ~packing:(table#attach ~left:1 ~top:0) ()
@@ -486,15 +499,19 @@ let configure ?(apply=(fun () -> ())) () =
       ~color:(Tags.get_error_color ())
       ~packing:(table#attach ~left:1 ~top:3) ()
     in
+    let error_fg_button = GButton.color_button
+      ~color:(Tags.get_error_fg_color ())
+      ~packing:(table#attach ~left:1 ~top:4) ()
+    in
     let reset_button = GButton.button
       ~label:"Reset"
       ~packing:box#pack ()
     in
     let reset_cb () =
-      background_button#set_color (Tags.color_of_string "cornsilk");
-      processing_button#set_color (Tags.color_of_string "light blue");
-      processed_button#set_color (Tags.color_of_string "light green");
-      error_button#set_color (Tags.color_of_string "#FFCCCC");
+      background_button#set_color Tags.(color_of_string default_color);
+      processing_button#set_color Tags.(color_of_string default_processing_color);
+      processed_button#set_color Tags.(color_of_string default_processed_color);
+      error_button#set_color Tags.(color_of_string default_error_color);
     in
     let _ = reset_button#connect#clicked ~callback:reset_cb in
     let label = "Color configuration" in
@@ -503,10 +520,12 @@ let configure ?(apply=(fun () -> ())) () =
       current.processing_color <- Tags.string_of_color processing_button#color;
       current.processed_color <- Tags.string_of_color processed_button#color;
       current.error_color <- Tags.string_of_color error_button#color;
+      current.error_fg_color <- Tags.string_of_color error_fg_button#color;
       !refresh_editor_hook ();
       Tags.set_processing_color processing_button#color;
       Tags.set_processed_color processed_button#color;
-      Tags.set_error_color error_button#color
+      Tags.set_error_color error_button#color;
+      Tags.set_error_fg_color error_fg_button#color
     in
     custom ~label box callback true
   in
diff --git a/ide/preferences.mli b/ide/preferences.mli
index 1b52d20a..1e4f152c 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;
 
@@ -71,6 +72,7 @@ type pref =
       mutable processing_color : string;
       mutable processed_color : string;
       mutable error_color : string;
+      mutable error_fg_color : string;
 
       mutable dynamic_word_wrap : bool;
       mutable show_line_number : bool;
diff --git a/ide/project_file.ml4 b/ide/project_file.ml4
index 41dc1bef..f7279f9c 100644
--- a/ide/project_file.ml4
+++ b/ide/project_file.ml4
@@ -182,29 +182,21 @@ let read_project_file f =
     (snd (process_cmd_line (Filename.dirname f) (Some f, None, NoInstall, true) [] (parse f)))
 
 let args_from_project file project_files default_name =
-  let is_f = CUnix.same_file file in
-  let contains_file dir =
-      List.exists (fun x -> is_f (CUnix.correct_path x dir))
-  in
   let build_cmd_line ml_inc i_inc r_inc args =
     List.fold_right (fun (_,i) o -> "-I" :: i :: o) ml_inc
       (List.fold_right (fun (_,l,i) o -> "-Q" :: i :: l :: o) i_inc
         (List.fold_right (fun (_,l,p) o -> "-R" :: p :: l :: o) r_inc
 	  (List.fold_right (fun a o -> parse_args (Stream.of_string a) @ o) args [])))
   in try
-      let (_,(_,(ml_inc,i_inc,r_inc),(args,_))) =
-	List.find (fun (dir,((v_files,_,_,_),_,_)) ->
-		     contains_file dir v_files) project_files in
-	build_cmd_line ml_inc i_inc r_inc args
-    with Not_found ->
+      let (fname,(_,(ml_inc,i_inc,r_inc),(args,_))) = List.hd project_files in
+	fname, build_cmd_line ml_inc i_inc r_inc args
+    with Failure _ ->
       let rec find_project_file dir = try
+	let fname = Filename.concat dir default_name in
 	let ((v_files,_,_,_),(ml_inc,i_inc,r_inc),(args,_)) =
-	  read_project_file (Filename.concat dir default_name) in
-	  if contains_file dir v_files
-	  then build_cmd_line ml_inc i_inc r_inc args
-	  else let newdir = Filename.dirname dir in
-	    if dir = newdir then [] else find_project_file newdir
+          read_project_file fname in
+	fname, build_cmd_line ml_inc i_inc r_inc args
       with Sys_error s ->
 	let newdir = Filename.dirname dir in
-	  if dir = newdir then [] else find_project_file newdir
+	  if dir = newdir then "",[] else find_project_file newdir
       in find_project_file (Filename.dirname file)
diff --git a/ide/session.ml b/ide/session.ml
index 29363211..12b77966 100644
--- a/ide/session.ml
+++ b/ide/session.ml
@@ -18,6 +18,7 @@ class type ['a] page =
     inherit GObj.widget
     method update : 'a -> unit
     method on_update : callback:('a -> unit) -> unit
+    method refresh_color : unit -> unit
   end
 
 class type control =
@@ -133,6 +134,11 @@ let set_buffer_handlers
     try ignore(buffer#get_mark (`NAME "stop_of_input"))
     with GText.No_such_mark _ -> assert false in
   let get_insert () = buffer#get_iter_at_mark `INSERT in
+  let update_prev it =
+    let prev = buffer#get_iter_at_mark (`NAME "prev_insert") in
+    if it#offset < prev#offset then
+      buffer#move_mark (`NAME "prev_insert") ~where:it
+  in
   let debug_edit_zone () = if false (*!Minilib.debug*) then begin
     buffer#remove_tag Tags.Script.edit_zone
       ~start:buffer#start_iter ~stop:buffer#end_iter;
@@ -147,10 +153,9 @@ let set_buffer_handlers
   let insert_cb it s = if String.length s = 0 then () else begin
     Minilib.log ("insert_cb " ^ string_of_int it#offset);
     let text_mark = add_mark it in
+    let () = update_prev it in
     if it#has_tag Tags.Script.to_process then
       cancel_signal "Altering the script being processed in not implemented"
-    else if it#has_tag Tags.Script.read_only then
-      cancel_signal "Altering read_only text not allowed"
     else if it#has_tag Tags.Script.processed then
       call_coq_or_cancel_action (coqops#go_to_mark (`MARK text_mark))
     else if it#has_tag Tags.Script.error_bg then begin
@@ -160,16 +165,14 @@ let set_buffer_handlers
     end end in
   let delete_cb ~start ~stop =
     Minilib.log (Printf.sprintf "delete_cb %d %d" start#offset stop#offset);
-    cur_action := new_action_id ();
     let min_iter, max_iter =
       if start#compare stop < 0 then start, stop else stop, start in
+    let () = update_prev min_iter in
     let text_mark = add_mark min_iter in
     let rec aux min_iter =
       if min_iter#equal max_iter then ()
       else if min_iter#has_tag Tags.Script.to_process then
         cancel_signal "Altering the script being processed in not implemented"
-      else if min_iter#has_tag Tags.Script.read_only then
-        cancel_signal "Altering read_only text not allowed"
       else if min_iter#has_tag Tags.Script.processed then
         call_coq_or_cancel_action (coqops#go_to_mark (`MARK text_mark))
       else if min_iter#has_tag Tags.Script.error_bg then
@@ -250,6 +253,10 @@ let make_table_widget cd cb =
       ~rules_hint:true ~headers_visible:false
       ~model:store ~packing:frame#add () in
   let () = data#set_headers_visible true in
+  let refresh () =
+    let clr = Tags.color_of_string current.background_color in
+    data#misc#modify_base [`NORMAL, `COLOR clr]
+  in
   let mk_rend c = GTree.cell_renderer_text [], ["text",c] in
   let cols =
     List.map2 (fun (_,c) (_,n,v) ->
@@ -265,10 +272,10 @@ let make_table_widget cd cb =
   ignore(
     data#connect#row_activated ~callback:(fun tp vc -> cb columns store tp vc)
   );
-  frame, (fun f -> f columns store)
+  frame, (fun f -> f columns store), refresh
 
 let create_errpage (script : Wg_ScriptView.script_view) : errpage =
-  let table, access =
+  let table, access, refresh =
     make_table_widget
       [`Int,"Line",true; `String,"Error message",true]
       (fun columns store tp vc ->
@@ -299,10 +306,11 @@ let create_errpage (script : Wg_ScriptView.script_view) : errpage =
           errs
       end
     method on_update ~callback:cb = callback := cb
+    method refresh_color () = refresh ()
   end
 
 let create_jobpage coqtop coqops : jobpage =
-  let table, access =
+  let table, access, refresh =
     make_table_widget
       [`String,"Worker",true; `String,"Job name",true]
       (fun columns store tp vc ->
@@ -338,6 +346,7 @@ let create_jobpage coqtop coqops : jobpage =
           jobs
       end
     method on_update ~callback:cb = callback := cb
+    method refresh_color () = refresh ()
   end
 
 let create_proof () =
@@ -465,7 +474,7 @@ let build_layout (sn:session) =
       message_frame#misc#show ();
       detachable#show);
     detachable#button#misc#hide ();
-    lbl in
+    detachable, lbl in
   let session_tab = GPack.hbox ~homogeneous:false () in
   let img = GMisc.image ~icon_size:`SMALL_TOOLBAR
     ~packing:session_tab#pack () in
@@ -496,9 +505,17 @@ let build_layout (sn:session) =
   sn.command#pack_in (session_paned#pack2 ~shrink:false ~resize:false);
   script_scroll#add sn.script#coerce;
   proof_scroll#add sn.proof#coerce;
-  ignore(add_msg_page 0 sn.tab_label#text "Messages" sn.messages#coerce);
-  let label = add_msg_page 1 sn.tab_label#text "Errors" sn.errpage#coerce in
-  ignore(add_msg_page 2 sn.tab_label#text "Jobs" sn.jobpage#coerce);
+  let detach, _ = add_msg_page 0 sn.tab_label#text "Messages" sn.messages#coerce in
+  let _, label = add_msg_page 1 sn.tab_label#text "Errors" sn.errpage#coerce in
+  let _, _ = add_msg_page 2 sn.tab_label#text "Jobs" sn.jobpage#coerce in
+  (** When a message is received, focus on the message pane *)
+  let _ =
+    sn.messages#connect#pushed ~callback:(fun _ _ ->
+      let num = message_frame#page_num detach#coerce in
+      if 0 <= num then message_frame#goto_page num
+    )
+  in
+  (** When an error occurs, paint the error label in red *)
   let txt = label#text in
   let red s = "<span foreground=\"#FF0000\">" ^ s ^ "</span>" in
   sn.errpage#on_update ~callback:(fun l ->
diff --git a/ide/session.mli b/ide/session.mli
index 3a6b4585..52e55721 100644
--- a/ide/session.mli
+++ b/ide/session.mli
@@ -14,6 +14,7 @@ class type ['a] page =
     inherit GObj.widget
     method update : 'a -> unit
     method on_update : callback:('a -> unit) -> unit
+    method refresh_color : unit -> unit
   end
 
 class type control =
diff --git a/ide/tags.ml b/ide/tags.ml
index 04ad9a51..c9b57af4 100644
--- a/ide/tags.ml
+++ b/ide/tags.ml
@@ -13,15 +13,23 @@ let make_tag (tt:GText.tag_table) ~name prop =
   tt#add new_tag#as_tag;
   new_tag
 
-let processed_color = ref "light green"
-let processing_color = ref "light blue"
-let error_color = ref "#FFCCCC"
+(* These work fine for colorblind people too *)
+let default_processed_color = "light green"
+let default_processing_color = "light blue"
+let default_error_color = "#FFCCCC"
+let default_error_fg_color = "red"
+let default_color = "cornsilk"
+
+let processed_color = ref default_processed_color
+let processing_color = ref default_processing_color
+let error_color = ref default_error_color
+let error_fg_color = ref default_error_fg_color
 
 module Script =
 struct
   let table = GText.tag_table ()
   let comment = make_tag table ~name:"comment" []
-  let error = make_tag table ~name:"error" [`UNDERLINE `SINGLE ; `FOREGROUND "red"]
+  let error = make_tag table ~name:"error" [`UNDERLINE `SINGLE ; `FOREGROUND !error_fg_color]
   let error_bg = make_tag table ~name:"error_bg" [`BACKGROUND !error_color]
   let to_process = make_tag table ~name:"to_process" [`BACKGROUND !processing_color]
   let processed = make_tag table ~name:"processed" [`BACKGROUND !processed_color]
@@ -44,8 +52,6 @@ struct
     t
   let all = edit_zone :: all
   
-  let read_only = make_tag table ~name:"read_only" [`EDITABLE false ]
-
 end
 module Proof =
 struct
@@ -94,3 +100,11 @@ let set_error_color clr =
   let s = string_of_color clr in
   error_color := s;
   Script.error_bg#set_property (`BACKGROUND s)
+
+let get_error_fg_color () = color_of_string !error_fg_color
+
+let set_error_fg_color clr =
+  let s = string_of_color clr in
+  error_fg_color := s;
+  Script.error#set_property (`FOREGROUND s)
+
diff --git a/ide/tags.mli b/ide/tags.mli
index 9c3261d6..14cfd0db 100644
--- a/ide/tags.mli
+++ b/ide/tags.mli
@@ -21,9 +21,6 @@ sig
   val tooltip : GText.tag
   val edit_zone : GText.tag (* for debugging *)
   val all : GText.tag list
-
-  (* Not part of the all list. Special tags! *)
-  val read_only : GText.tag
 end
 
 module Proof :
@@ -53,3 +50,13 @@ val set_processing_color : Gdk.color -> unit
 
 val get_error_color : unit -> Gdk.color
 val set_error_color : Gdk.color -> unit
+
+val get_error_fg_color : unit -> Gdk.color
+val set_error_fg_color : Gdk.color -> unit
+
+val default_processed_color : string
+val default_processing_color : string
+val default_error_color : string
+val default_error_fg_color : string
+val default_color : string
+
diff --git a/ide/wg_Find.ml b/ide/wg_Find.ml
index b6f63a3b..a0949ca0 100644
--- a/ide/wg_Find.ml
+++ b/ide/wg_Find.ml
@@ -8,6 +8,8 @@
 
 type mode = [ `FIND | `REPLACE ]
 
+let b2c = Ideutils.byte_offset_to_char_offset
+
 class finder name (view : GText.view) =
   
   let widget = Wg_Detachable.detachable
@@ -61,8 +63,10 @@ class finder name (view : GText.view) =
     method replace () =
       if self#may_replace () then
         let txt = self#get_selected_word () in
+        let () = view#buffer#begin_user_action () in
         let _ = view#buffer#delete_selection () in
         let _ = view#buffer#insert_interactive (self#replacement txt) in
+        let () = view#buffer#end_user_action () in
         self#find_forward ()
       else self#find_forward ()
 
@@ -85,8 +89,8 @@ class finder name (view : GText.view) =
       try
         let i = Str.search_backward regexp text (String.length text - 1) in
         let j = Str.match_end () in
-        Some(view#buffer#start_iter#forward_chars i,
-             view#buffer#start_iter#forward_chars j)
+        Some(view#buffer#start_iter#forward_chars (b2c text i),
+             view#buffer#start_iter#forward_chars (b2c text j))
       with Not_found -> None
     
     method private forward_search starti =
@@ -95,7 +99,7 @@ class finder name (view : GText.view) =
       try
         let i = Str.search_forward regexp text 0 in
         let j = Str.match_end () in
-        Some(starti#forward_chars i, starti#forward_chars j)
+        Some(starti#forward_chars (b2c text i), starti#forward_chars (b2c text j))
       with Not_found -> None
 
     method replace_all () =
@@ -115,7 +119,9 @@ class finder name (view : GText.view) =
           let () = view#buffer#delete_mark (`MARK stop_mark) in
           replace_at next
       in
-      replace_at view#buffer#start_iter
+      let () = view#buffer#begin_user_action () in
+      let () = replace_at view#buffer#start_iter in
+      view#buffer#end_user_action ()
 
     method private set_not_found () =
       find_entry#misc#modify_base [`NORMAL, `NAME "#F7E6E6"];
diff --git a/ide/wg_MessageView.ml b/ide/wg_MessageView.ml
index 9acda53f..211db537 100644
--- a/ide/wg_MessageView.ml
+++ b/ide/wg_MessageView.ml
@@ -6,9 +6,25 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+class type message_view_signals =
+object
+  inherit GObj.misc_signals
+  inherit GUtil.add_ml_signals
+  method pushed : callback:(Pp.message_level -> string -> unit) -> GtkSignal.id
+end
+
+class message_view_signals_impl obj (pushed : 'a GUtil.signal) : message_view_signals =
+object
+  val after = false
+  inherit GObj.misc_signals obj
+  inherit GUtil.add_ml_signals obj [pushed#disconnect]
+  method pushed ~callback = pushed#connect ~after ~callback:(fun (lvl, s) -> callback lvl s)
+end
+
 class type message_view =
   object
     inherit GObj.widget
+    method connect : message_view_signals
     method clear : unit
     method add : string -> unit
     method set : string -> unit
@@ -17,6 +33,7 @@ class type message_view =
     method buffer : GText.buffer
       (** for more advanced text edition *)
     method modify_font : Pango.font_description -> unit
+    method refresh_color : unit -> unit
   end
 
 let message_view () : message_view =
@@ -32,12 +49,18 @@ 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
   object (self)
     inherit GObj.widget box#as_widget
 
+    val push = new GUtil.signal ()
+
+    method connect =
+      new message_view_signals_impl box#as_widget push
+
     method clear =
       buffer#set_text ""
 
@@ -49,7 +72,8 @@ let message_view () : message_view =
       in
       if msg <> "" then begin
         buffer#insert ~tags msg;
-        buffer#insert ~tags "\n"
+        buffer#insert ~tags "\n";
+        push#call (level, msg)
       end
 
     method add msg = self#push Pp.Notice msg
@@ -60,4 +84,9 @@ let message_view () : message_view =
 
     method modify_font fd = view#misc#modify_font fd
 
+    method refresh_color () =
+      let open Preferences in
+      let clr = Tags.color_of_string current.background_color in
+      view#misc#modify_base [`NORMAL, `COLOR clr]
+
   end
diff --git a/ide/wg_MessageView.mli b/ide/wg_MessageView.mli
index cd3f00c9..23c94f40 100644
--- a/ide/wg_MessageView.mli
+++ b/ide/wg_MessageView.mli
@@ -6,9 +6,17 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+class type message_view_signals =
+object
+  inherit GObj.misc_signals
+  inherit GUtil.add_ml_signals
+  method pushed : callback:(Pp.message_level -> string -> unit) -> GtkSignal.id
+end
+
 class type message_view =
   object
     inherit GObj.widget
+    method connect : message_view_signals
     method clear : unit
     method add : string -> unit
     method set : string -> unit
@@ -17,6 +25,7 @@ class type message_view =
     method buffer : GText.buffer
       (** for more advanced text edition *)
     method modify_font : Pango.font_description -> unit
+    method refresh_color : unit -> unit
   end
 
 val message_view : unit -> message_view
diff --git a/ide/wg_ProofView.ml b/ide/wg_ProofView.ml
index 7e7a311e..b12d29d6 100644
--- a/ide/wg_ProofView.ml
+++ b/ide/wg_ProofView.ml
@@ -9,6 +9,7 @@
 class type proof_view =
   object
     inherit GObj.widget
+    method buffer : GText.buffer
     method refresh : unit -> unit
     method clear : unit -> unit
     method set_goals : Interface.goals option -> unit
@@ -176,9 +177,11 @@ let proof_view () =
     ~highlight_matching_brackets:true
     ~tag_table:Tags.Proof.table ()
   in
+  let text_buffer = new GText.buffer buffer#as_buffer in
   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
@@ -186,6 +189,8 @@ let proof_view () =
     val mutable goals = None
     val mutable evars = None
 
+    method buffer = text_buffer
+
     method clear () = buffer#set_text ""
 
     method set_goals gls = goals <- gls
diff --git a/ide/wg_ProofView.mli b/ide/wg_ProofView.mli
index 1fbf9900..c5e042ea 100644
--- a/ide/wg_ProofView.mli
+++ b/ide/wg_ProofView.mli
@@ -9,6 +9,7 @@
 class type proof_view =
   object
     inherit GObj.widget
+    method buffer : GText.buffer
     method refresh : unit -> unit
     method clear : unit -> unit
     method set_goals : Interface.goals option -> unit
diff --git a/ide/wg_ScriptView.ml b/ide/wg_ScriptView.ml
index 1f399070..8298d995 100644
--- a/ide/wg_ScriptView.ml
+++ b/ide/wg_ScriptView.ml
@@ -186,11 +186,19 @@ object(self)
 
   method undo () =
     Minilib.log "UNDO";
-    self#with_lock_undo self#perform_undo ();
+    self#with_lock_undo begin fun () ->
+      buffer#begin_user_action ();
+      self#perform_undo ();
+      buffer#end_user_action ()
+    end ()
 
   method redo () =
     Minilib.log "REDO";
-    self#with_lock_undo self#perform_redo ();
+    self#with_lock_undo begin fun () ->
+      buffer#begin_user_action ();
+      self#perform_redo ();
+      buffer#end_user_action ()
+    end ()
 
   method process_begin_user_action () =
     (* Push a new level of event on history stack *)
@@ -410,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()
diff --git a/ide/wg_Segment.ml b/ide/wg_Segment.ml
index 8520727a..25a031d6 100644
--- a/ide/wg_Segment.ml
+++ b/ide/wg_Segment.ml
@@ -70,9 +70,25 @@ let color_eq (c1 : GDraw.color) (c2 : GDraw.color) = match c1, c2 with
 | `WHITE, `WHITE -> true
 | _ -> false
 
+class type segment_signals =
+object
+  inherit GObj.misc_signals
+  inherit GUtil.add_ml_signals
+  method clicked : callback:(int -> unit) -> GtkSignal.id
+end
+
+class segment_signals_impl obj (clicked : 'a GUtil.signal) : segment_signals =
+object
+  val after = false
+  inherit GObj.misc_signals obj
+  inherit GUtil.add_ml_signals obj [clicked#disconnect]
+  method clicked = clicked#connect ~after
+end
+
 class segment () =
 let box = GBin.frame () in
-let draw = GMisc.image ~packing:box#add () in
+let eventbox = GBin.event_box ~packing:box#add () in
+let draw = GMisc.image ~packing:eventbox#add () in
 object (self)
 
   inherit GObj.widget box#as_widget
@@ -82,6 +98,7 @@ object (self)
   val mutable data = Segment.empty
   val mutable default : color = `WHITE
   val mutable pixmap : GDraw.pixmap = GDraw.pixmap ~width:1 ~height:1 ()
+  val clicked = new GUtil.signal ()
 
   initializer
     box#misc#set_size_request ~height ();
@@ -96,6 +113,15 @@ object (self)
       end
     in
     let _ = box#misc#connect#size_allocate cb in
+    let clicked_cb ev =
+      let x = GdkEvent.Button.x ev in
+      let (width, _) = pixmap#size in
+      let len = Segment.length data in
+      let idx = f2i ((x *. i2f len) /. i2f width) in
+      let () = clicked#call idx in
+      true
+    in
+    let _ = eventbox#event#connect#button_press clicked_cb in
     (** Initial pixmap *)
     draw#set_pixmap pixmap
 
@@ -140,4 +166,7 @@ object (self)
     Segment.fold color_eq fold data ();
     draw#set_mask None;
 
+  method connect =
+    new segment_signals_impl box#as_widget clicked
+
 end
diff --git a/ide/wg_Segment.mli b/ide/wg_Segment.mli
index ecb45147..0263856a 100644
--- a/ide/wg_Segment.mli
+++ b/ide/wg_Segment.mli
@@ -8,10 +8,18 @@
 
 type color = GDraw.color
 
+class type segment_signals =
+object
+  inherit GObj.misc_signals
+  inherit GUtil.add_ml_signals
+  method clicked : callback:(int -> unit) -> GtkSignal.id
+end
+
 class segment : unit ->
   object
     inherit GObj.widget
     val obj : Gtk.widget Gtk.obj
+    method connect : segment_signals
     method length : int
     method set_length : int -> unit
     method default_color : color